Recursion on nested datatypes within dependent type theory
All the following code is additional material to the article of the
same name by the author that was presented at CiE'08 (included in the LNCS proceedings).
The latter three come from the extra material for the JFP paper
this work is based on (my publications page).
A version with tiny modifications to run in version 8.4 of Coq (tested with 8.4pl1 in December 2012):
Ralph Matthes