proposition: Lemma member_multiset_list : forall l, forall x, member x (list2multiset l) -> exists2 y, In y l & x =A= y.
proof: Proof. induction l. simpl; intros x x_in_empty. absurd (empty <>mul empty); eauto with multisets. unfold insert; simpl; intros x x_in_al. case (member_union x_in_al). intro x_a; exists a; auto with multisets. intro x_l; destruct (IHl x x_l). exists x0; auto with sets. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)