proposition: Lemma double_convertion : forall M, list2multiset (multiset2list M) =mul= M.
proof: Proof. induction M as [ | M a IHM] using mset_ind. rewrite multiset2list_empty; simpl; auto with multisets. unfold multiset2list; elim (mult_to_list (M + {{a}})). intros l Hl. rewrite Hl; auto with multisets. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)