proposition: Lemma typing_c_subst : forall (E F : env) e u S T (z : atom), typing_c (F ++ (z ~ S) ++ E) e T -> typing_c E u S -> typing_c (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_c". intros F Eq. subst. eapply typing_subst_var_case. apply H0. apply H. apply Hu. Case "typing_abs_c". intros F Eq. subst. simpl. pick fresh y and apply typing_abs_c. rewrite subst_open_var_c. rewrite_env (((y ~ T1) ++ F) ++ E). apply H0. auto. simpl_env. reflexivity. auto. eapply typing_c_to_lc_c. apply Hu. Case "typing_app_c". intros F Eq. subst. simpl. eapply typing_app_c. apply IHHe1. reflexivity. apply IHHe2. reflexivity. Qed.
imports: Metalib.Metatheory String