intros M wf_el
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
⊢ ∀ (M : Multiset α), (∀ x ∈ M, Acc LT.lt x) → AccM_1 M
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M : Multiset α
wf_el : ∀ x ∈ M, Acc LT.lt x
⊢ AccM_1 M