proposition: Lemma multiset2list_card M : length (multiset2list M) = card M.
proof: Proof. intros. unfold card; destruct (card_def M); trivial. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)