proposition: Lemma multiset2list_singleton a : exists a', a =A= a' /\ multiset2list {{a}} = a' :: nil.
proof: Proof. unfold multiset2list. destruct (mult_to_list {{a}}). destruct x; simpl in m. exfalso; apply not_empty with {{a}} a; trivial. unfold member; rewrite singleton_mult_in; auto with sets. destruct x; simpl in m. unfold insert in m. destruct (eqA_dec a a0). exists a0; split; trivial. exfalso. absurd (a/{{a}} = a/{{a0}}). rewrite singleton_mult_in with a a; auto with sets. rewrite singleton_mult_notin with a a0; auto with sets. apply meq_multeq. rewrite m; auto with multisets. exfalso. apply cons_eq_cons_cons_absurd with a a0 a1 (list2multiset x). rewrite m; solve_meq. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)