proposition: Lemma preservation : forall (E : ctx) e e' T, typing E e T -> step e e' -> typing E e' T.
proof: Proof. intros E e e' T H. generalize dependent e'. induction H; intros e' J. Case "typing_var". inversion J. Case "typing_abs". inversion J. Case "typing_app". inversion J; subst; eauto. SCase "step_beta". inversion H; subst. pick fresh y for (L \u fv_exp e0). rewrite (subst_exp_intro y); auto. eapply typing_subst_simple; auto. Qed.
imports: String Metalib.Metatheory Stlc.Definitions Stlc.Lemmas Stlc.Lec1