induction H0 with
| intro x wfH wfH2 =>
  apply mord_wf_1
  . simpa
  . intros b x a
    unfold AccM_1
    apply H
    assumption
  . constructor
    simpa
  . simpa
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
H : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
M : Multiset α
H0 : Acc MultisetRedLt M
⊢ Acc MultisetRedLt (a ::ₘ M)
no goals