proposition: Lemma tlt_mpo_eqA_compat : forall x x' y y', eqA x x' -> eqA y y' -> transp lt_mpo x y -> transp lt_mpo x' y'.
proof: Proof. unfold eqA,Term.eqA; intros; subst; trivial. Qed.
imports: CoLoR(AccUtil MultisetOrder ListExtras RelExtras MultisetCore MultisetList MultisetTheory MultisetListOrder VTerm RelUtil LogicUtil) Coq(Permutation Arith Setoid)