proposition: Lemma nonempty_mset_ind : forall (P : Multiset -> Prop), (forall M N, P M -> M =mul= N -> P N) -> (forall a, P {{a}}) -> (forall a M, P M -> P (M+{{a}})) -> forall M : Multiset, M <>mul empty -> P M.
proof: Proof. intros P P_morph Ha HMa M; induction M using mset_ind. intro H; elim H; auto with multisets. intros H; clear H. elim (empty_dec M); intro case_M. apply (P_morph {{a}}). apply Ha. rewrite case_M; solve_meq. apply HMa; apply IHM; hyp. Qed.
imports: Coq(List Permutation Arith Morphisms Basics) CoLoR(MultisetOrder RelExtras MultisetCore MultisetList MultisetTheory AccUtil RelUtil LogicUtil) CoLoR(AccUtil ListUtil)