proposition: Lemma typing_subst_var_case : forall (E F : env) u S T (z x : atom), binds x T (F ++ (z ~ S) ++ E) -> uniq (F ++ (z ~ S) ++ E) -> typing_c E u S -> typing_c (F ++ E) ([z ~> u] x) T.
proof: Proof. intros E F u S T z x H J K. simpl. destruct (x == z). Case "x = z". subst. assert (T = S). eapply binds_mid_eq. apply H. apply J. subst. apply typing_c_weakening. apply K. eapply uniq_remove_mid. apply J. Case "x <> z". apply typing_var_c. eapply uniq_remove_mid. apply J. eapply binds_remove_mid. apply H. apply n. Qed.
imports: Metalib.Metatheory String