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