Map Fusion 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 is to appear in Science of Computer Programming.

The current version was put here on February 2, 2010.

LNMItPred.v (Version 2.7)
LNMItImp.v (Version 2.5)
LNGMItPred.v (Version 1.5)
LNGMItImp.v (Version 1.3a)
LamFlatPred.v (Version 1.1)
README.txt
PDF of coqdoc of predicative development (first, third and fifth file)
PDF of coqdoc of impredicative development (second and fourth file)
a ZIP file with everything

The old MPC'08 development is here.