proposition: Lemma mord_wf_3: forall a, AccA a -> forall M, AccM_1 M -> AccM_1 (M + {{a}}).
proof: Proof. intros a a_wf. apply Acc_ind with (P := fun a => forall M, AccM_1 M -> AccM_1 (M + {{a}})) (R := ltA); trivial. intros; apply mord_wf_2; trivial. intros; apply H0; trivial. Qed.
imports: Coq(Transitive_Closure Compare_dec Relations Permutation Setoid Morphisms Basics Lia) CoLoR(RelExtras MultisetTheory ListPermutation MultisetCore ListExtras AccUtil LogicUtil)