proposition: Lemma typing_weakening : forall (E F : ctx) e T, typing E e T -> uniq (F ++ E) -> typing (F ++ E) e T.
proof: Proof. intros E F e T H J. rewrite_env (nil ++ F ++ E). apply typing_weakening_strengthened; auto. Qed.
imports: String Metalib.Metatheory Stlc.Definitions Stlc.Lemmas Stlc.Lec1