proposition: Lemma typing_c_uniq : forall E e T, typing_c E e T -> uniq E.
proof: Proof. intros E e T H. induction H; auto. Case "typing_abs_c". pick fresh x. assert (uniq ((x ~ T1) ++ E)); auto. inversion H1. auto. Qed.
imports: Metalib.Metatheory String