Cleanup proofs at the end of Imp.v
Completed ImpCEvalFun.v
Progress on Equiv.v