Using Coq to Understand Nested Datatypes. - Antonio Blanco; J. E. Freire; José Luis Freire (EUROCAST, 2007)