proposition: Lemma term_eq_correct : forall t u, term_eq (t, u) = true -> t = u.
proof: Proof. intros. unfold term_eq in H. destruct (term_eq_dec t u). hyp. discr. Qed.
imports: CoLoR(VRPO_Type VTerm Preorder ListUtil RelUtil LogicUtil AccUtil) Coq(Peano_dec)