proposition: Lemma SPO_to_status_SPO : forall f (r : relation term), forall ss, (forall s, In s ss -> (forall t u, r s t -> r t u -> r s u) /\ (r s s -> False)) -> (forall ts us, tau f r ss ts -> tau f r ts us -> tau f r ss us) /\ (tau f r ss ss -> False).
proof: Proof. intros f r. unfold tau, mytau. intros. apply transp_SPO_to_mult_SPO; trivial. unfold eqA, Term.eqA; intros; subst; trivial. unfold eqA, Term.eqA; intros; subst; trivial. Qed.
imports: CoLoR(VPrecedence MultisetListOrder VRPO_Type VTerm ListUtil AccUtil LogicUtil) Coq(Relations) CoLoR(VRPO_Type)