proposition: Lemma typing_c_rename : forall (x y : atom) E e T1 T2, x `notin` fv e -> y `notin` (dom E `union` fv e) -> typing_c ((x ~ T1) ++ E) (open e x) T2 -> typing_c ((y ~ T1) ++ E) (open 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_c_uniq; eauto. assert (J' : uniq E). inversion J; eauto. rewrite (@subst_intro x); eauto. rewrite_env (nil ++ (y ~ T1) ++ E). apply typing_c_subst with (S := T1). simpl_env. SCase "(open x s) is well-typed". apply typing_c_weakening_strengthened. eauto. auto. SCase "y is well-typed". eapply typing_var_c; eauto. Qed.
imports: Metalib.Metatheory String