proposition: Lemma typing_subst : forall (E F : ctx) e u S T (z : atom), typing (F ++ [(z,S)] ++ E) e T -> typing E u S -> typing (F ++ E) ([z ~> u] e) T.
proof: Proof. intros E F e u S T z He Hu. remember (F ++ [(z,S)] ++ E) as E'. generalize dependent F. induction He. - Case "typing_var". intros F Eq. subst. eapply typing_subst_var_case. apply H0. apply H. apply Hu. - Case "typing_abs". intros F Eq. subst. simpl. apply typing_abs with (L := {{z}} \u L). intros y Fry. rewrite subst_var. rewrite_env (([(y,T1)] ++ F) ++ E). apply H0. auto. simpl_env. reflexivity. auto. eapply typing_to_lc_exp. apply Hu. - Case "typing_app". intros F Eq. subst. simpl. eapply typing_app. apply IHHe1. reflexivity. apply IHHe2. reflexivity. Qed.
imports: String Metalib.Metatheory Stlc.Definitions Stlc.Lemmas Stlc.Lec1