proposition: Lemma list2multiset_app : forall M1 M2, list2multiset (M1 ++ M2) =mul= list2multiset M1 + list2multiset M2.
proof: Proof. induction M1; intros. simpl. eauto with multisets. simpl. unfold insert. rewrite (IHM1 M2). solve_meq. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)