proposition: Lemma typing_uniq : forall M N, env M = env N -> term M = term N -> type M = type N.
proof: Proof. intros; destruct M as [??? typingM]; destruct N as [??? typingN]; simpl in *. revert typingM. rewrite H; rewrite H0; intros. apply (Type_unique typingM typingN). Qed.
imports: Coq(Eqdep_dec) CoLoR(RelExtras ListExtras LogicUtil)