proposition: Lemma mono_axiom : forall f (r : relation term), forall ss ts, one_less r ss ts -> tau f r ss ts.
proof: Proof. intros f r ss ts. unfold tau, mytau. apply one_less2mult. unfold eqA, Term.eqA; intros; subst; trivial. Qed.
imports: CoLoR(VPrecedence MultisetListOrder VRPO_Type VTerm ListUtil AccUtil LogicUtil) Coq(Relations) CoLoR(VRPO_Type)