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 is accepted for presentation at CiE'08.

The latter three come from the extra material for the JFP paper this work is based on (my publications page).