proposition: Lemma list2multiset_eq_length l l' : list2multiset l =mul= list2multiset l' -> length l = length l'.
proof: Proof. intros. apply permutation_length with eqA eqA_dec. exact eqA_Equivalence. apply meq_permutation; trivial. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)