proposition: Lemma permutation_meq l l' : permutation eqA_dec l l' -> list2multiset l =mul= list2multiset l'.
proof: Proof. intros. apply multeq_meq. intro x. rewrite !list2multiset_mult. apply H. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)