proposition: Lemma eval_c_to_eval : forall e e', eval_c e e' -> eval e e'.
proof: Proof. Admitted. Lemma preservation : forall E e e' T, typing E e T -> eval e e' -> typing E e' T. 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