proposition: Lemma typing_rename : forall (x y : atom) E e T1 T2, x `notin` fv_exp e -> y `notin` dom E -> typing ([(x, T1)] ++ E) (e ^ x) T2 -> typing ([(y, T1)] ++ E) (e ^ y) T2.
proof: Proof. intros x y E e T1 T2 Fr1 Fr2 H. destruct (x == y). - Case "x = y". subst; eauto. - Case "x <> y". assert (J : uniq ([(x, T1)] ++ E)). eapply typing_uniq; eauto. assert (J' : uniq E). inversion J; eauto. rewrite (@subst_exp_intro x); eauto. rewrite_env (nil ++ [(y, T1)] ++ E). apply typing_subst with (S := T1). simpl_env. + SCase "(open x s) is well-typed". apply typing_weakening_strengthened. eauto. auto. + SCase "y is well-typed". eapply typing_var; eauto. Qed.
imports: String Metalib.Metatheory Stlc.Definitions Stlc.Lemmas Stlc.Lec1