proposition: Lemma eq_Term_dec : forall (M N: Term), {M=N} + {M<>N}.
proof: Proof. intros M N. case (eq_Env_dec M.(env) N.(env)); case (eq_Preterm_dec M.(term) N.(term)); case (eq_SimpleType_dec M.(type) N.(type)); try solve [right; congruence]. left; apply deriv_uniq; trivial. Qed.
imports: Coq(Eqdep_dec) CoLoR(RelExtras ListExtras LogicUtil)