Coq proofs from "Contracts Made Manifest" (Greenberg, Pierce, and Weirich POPL 2010).
The lambdah_parred.tgz file should have a working version of the Metatheory library packaged with it.
This Coq development is essentially crapware, and is not maintained. I'm sorry.