Arthur Charguéraud's de Bruijn solution

• Author: Arthur Charguéraud.
• Parts addressed: 1a.
• Proof assistant / theorem prover used: Coq.
• Encoding technique: De Bruijn indices, variable labelling, implicit environments.
• Files: available from the author's page.

Commentary

This solution is based on a different technique to handle well-formation, and also it uses two tricks: labelling free variables with the type they are bound to and then making the environment implicit. This work has been greatly influanced by Jérôme Vouillon's solution, and also some tactics and methods from Xavier Leroy's code were used.