COQ files for TYPES 2006 article

The following files are the Coq development for the results reported in the article Combining de Bruijn Indices and Higher-Order Abstract Syntax in Coq by Venanzio Capretta and Amy P. Felty, to appear in the Proceedings of TYPES 2006. De Bruijn syntax is needed for the Lambda Calculus and Quantified Propositional Logic. You need first to compile deBruijn.v with the command:
coqc deBruijn.v
to be able to run Lambda.v and QPL.v.