proposition: Lemma typing_subst_simple : forall (E : ctx) e u S T (z : atom), typing ([(z,S)] ++ E) e T -> typing E u S -> typing E ([z ~> u] e) T.
proof: Proof. intros E e u S T z H J. rewrite_env (nil ++ E). eapply typing_subst. simpl_env. apply H. apply J. Qed.
imports: String Metalib.Metatheory Stlc.Definitions Stlc.Lemmas Stlc.Lec1