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