Jérôme Vouillon's solution


This solution offers an excellent baseline against which to measure others: the representation technique (pure deBruijn) is one of the simplest and most concrete imaginable, and some of the development is correspondingly concerned with low-level details of index manipulation, etc. However, by appropriate choices of tactics and and low-level lemmas, these low-level details are largely kept from polluting the main definitions or theorems, which closely follow the paper presentation.