prove the Opapp case of exp_to_Cexp_correct

this is a good sign that the theorem statement is now correct; should
check the Letrec case also.