An induction principle for nested datatypes in intensional type theory

All the following code is additional material to the article of the same name by the author that appeared in the Journal of Functional Programming in June 2009 (online version at CUP)) Its version is 2.0 (January 2008) and also recognizable in having 8.1pl3 as test system. It has also been tested with Coq 8.2 (version 8.2-1).

A version with tiny modifications to run in version 8.4 of Coq (tested with 8.4pl1 in December 2012) that also runs in version 8.5 of Coq (tested with 8.5pl2 of July 2016):

Ralph Matthes