proposition: Lemma in_multiset_in_multiset2list : forall M x, x in M -> exists y, x =A= y /\ In y (multiset2list M).
proof: Proof. destruct M using mset_ind. intros x abs. absurd (empty =mul= empty); auto with multisets. apply member_notempty with x; trivial. unfold multiset2list. elim (mult_to_list (M + {{a}})). intros l Ml x xin. assert (x in (list2multiset l)). rewrite <- Ml; trivial. destruct (member_multiset_list l H). exists x0; auto. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)