Coq proofs from Contracts Made Manifest [Greenberg, Pierce, Weirich POPL 2010]