proposition: Lemma mred_acc : forall M, (forall x, x in M -> AccA x) -> AccM_1 M.
proof: Proof. intros M wf_el. induction M using mset_ind. constructor; intros y y_lt; absurd (empty >mul_1 y); auto with multisets. apply mord_wf_3. apply wf_el; auto with multisets. apply IHM; intros; apply wf_el; auto with multisets. Qed.
imports: Coq(Transitive_Closure Compare_dec Relations Permutation Setoid Morphisms Basics Lia) CoLoR(RelExtras MultisetTheory ListPermutation MultisetCore ListExtras AccUtil LogicUtil)