induction w_a with
| intro x _ ih =>
    intro M accM1
    apply @mord_wf_2 α _ _ _ _ _ accM1
    simp_all
α : Type u
x✝ : Multiset α
inst✝¹ : DecidableEq α
inst✝ : Preorder α
w : α
w_a : Acc LT.lt w
⊢ ∀ (M : Multiset α), AccM_1 M → AccM_1 (w ::ₘ M)
no goals