proposition: Lemma multiset2list_meq_empty : forall M, M =mul= empty -> multiset2list M = nil.
proof: Proof. destruct M using mset_ind. unfold multiset2list. elim (mult_to_list empty). destruct x; trivial. simpl; intro abs. absurd (insert a (list2multiset x) =mul= empty); auto with multisets. apply member_notempty with a; unfold insert; auto with multisets. intro abs. absurd (M + {{a}} =mul= empty); trivial. apply member_notempty with a; trivial. apply member_union_r; auto with multisets. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)