proposition: Lemma mord_acc_mOrd_acc : forall x, AccM x -> ACC_M x.
proof: Proof. intros. unfold ACC_M. apply Acc_homo with Multiset MultisetLt (fun x y : Multiset => x = y) x; trivial. intros. exists y; trivial. unfold MultisetLt, transp; simpl. apply direct_subset_red. rewrite H0; trivial. Qed.
imports: Coq(Transitive_Closure Compare_dec Relations Permutation Setoid Morphisms Basics Lia) CoLoR(RelExtras MultisetTheory ListPermutation MultisetCore ListExtras AccUtil LogicUtil)