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))

the six Coq vernacular files with the implementation and the README
LNMItPred.v
LNMItImp.v
BushPred.v
BushImp.v
EFlatCoqPred.v
EFlatCoqImp.v
README.txt

The current 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).

Ralph Matthes