proposition: Lemma mord_wf_2: forall a, (forall b M, b <A a -> AccM_1 M -> AccM_1 (M + {{b}})) -> forall M, AccM_1 M -> AccM_1 (M + {{a}}).
proof: Proof. unfold AccM_1; intros. apply Acc_ind with (P := fun M => AccM_1 (M + {{a}})) (R := MultisetRedLt). intros x wfH wfH2; apply mord_wf_1; intros; unfold AccM_1. apply H; trivial. constructor; trivial. apply wfH2; trivial. trivial. Qed.
imports: Coq(Transitive_Closure Compare_dec Relations Permutation Setoid Morphisms Basics Lia) CoLoR(RelExtras MultisetTheory ListPermutation MultisetCore ListExtras AccUtil LogicUtil)