proposition: Lemma multiset2list_meq_non_empty : forall M, M <>mul empty -> multiset2list M <> nil.
proof: Proof. destruct M using mset_ind. auto with multisets. intros _. unfold multiset2list; elim (mult_to_list (M + {{a}})). destruct x; auto with datatypes. simpl; 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)