This is a very hastily-written notation-less implementation of lambda2 system in Coq.
For more information, see chapter three of Type Theory and Formal Proof, an Introduction, by Nederpelt and Geuvers.