proposition: Lemma meq_permutation l l' : list2multiset l =mul= list2multiset l' -> permutation eqA_dec l l'.
proof: Proof. intros; intro a. rewrite <- !list2multiset_mult. apply meq_multeq; trivial. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)