proposition: Lemma typing_subst_var_case : forall (E F : ctx) u S T (z x : atom), binds x T (F ++ [(z,S)] ++ E) -> uniq (F ++ [(z,S)] ++ E) -> typing E u S -> typing (F ++ E) ([z ~> u] (var_f 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_weakening. apply K. eapply uniq_remove_mid. apply J. Case "x <> z". apply typing_var. eapply uniq_remove_mid. apply J. eapply binds_remove_mid. apply H. apply n. Qed.
imports: String Metalib.Metatheory Stlc.Definitions Stlc.Lemmas Stlc.Lec1