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