proposition: Lemma Acc_multiset_list : transitive r -> forall ss, Acc (MultisetLt r) (list2multiset ss) -> Acc mult ss.
proof: Proof. intros r_trans ss Hacc. unfold mult; apply (Acc_inverse_image (list A) Multiset (MultisetLT r) list2multiset ss). gen Hacc; apply Acc_eq_rel. unfold MultisetLt,MultisetLT,transp; simpl; intros a b; apply red_eq_direct; trivial. intros x y xy u v uv xu. eapply r_eqA_compat. apply xy. apply uv. hyp. Qed.
imports: Coq(List Permutation Arith Morphisms Basics) CoLoR(MultisetOrder RelExtras MultisetCore MultisetList MultisetTheory AccUtil RelUtil LogicUtil) CoLoR(AccUtil ListUtil)