fact: Definition le_mpo := fun t s => t = s \/ lt_mpo t s.
imports: CoLoR(AccUtil MultisetOrder ListExtras RelExtras MultisetCore MultisetList MultisetTheory MultisetListOrder VTerm RelUtil LogicUtil) Coq(Permutation Arith Setoid)