proposition: Lemma preservation : forall E e e' T, typing E e T -> eval e e' -> typing E e' T.
proof: Proof. intros E e e' T HT HE. apply typing_c_to_typing. eapply preservation_c; eauto. eapply typing_to_typing_c. eauto. apply eval_to_eval_c. auto. Qed.
imports: Metalib.Metatheory String