proposition: Lemma typing_uniq : forall E e T, typing E e T -> uniq E.
proof: Proof. intros E e T H. induction H; auto. - Case "typing_abs". pick fresh x. assert (uniq ([(x, T1)] ++ G)); auto. solve_uniq. Qed.
imports: String Metalib.Metatheory Stlc.Definitions Stlc.Lemmas Stlc.Lec1