apply mred_acc
case h
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
wf_lt : WellFoundedLT α
a : Multiset α
⊢ Acc MultisetRedLt a
case h.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
wf_lt : WellFoundedLT α
a : Multiset α
⊢ ∀ x ∈ a, Acc LT.lt x