proposition: Lemma mset_ind : forall P : Multiset -> Prop, P empty -> (forall M a, P M -> P (M + {{a}})) -> forall M, P M.
proof: Proof. exact mset_ind_type. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)