constructor
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
wf_lt : WellFoundedLT α
⊢ WellFounded MultisetRedLt
case h
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
wf_lt : WellFoundedLT α
⊢ ∀ (a : Multiset α), Acc MultisetRedLt a