Arthur Charguéraud's de Bruijn solution

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.