proposition: Lemma multiset2list_meq_length M M' : M =mul= M' -> length (multiset2list M) = length (multiset2list M').
proof: Proof. intros; unfold multiset2list. destruct (mult_to_list M); destruct (mult_to_list M'); simpl. apply list2multiset_eq_length. rewrite <- m; rewrite <- m0; trivial. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)