proposition: Lemma in_multiset2list_in_multiset : forall M x, In x (multiset2list M) -> x in M.
proof: Proof. destruct M using mset_ind. rewrite multiset2list_empty. inversion 1. unfold multiset2list. destruct (mult_to_list (M + {{a}})) as [l Mal]; intros x xl. rewrite Mal. apply member_list_multiset; trivial. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)