proposition: Lemma mset_ind_type : forall P : Multiset -> Type, P empty -> (forall M a, P M -> P (union M {{a}})) -> forall M, P M.
proof: Proof. induction M as [| x M] using rev_ind_type. exact X. exact (X0 M x IHM). Defined.
imports: Coq(Permutation PermutSetoid Lia Multiset) CoLoR(LogicUtil RelExtras MultisetCore ListExtras)