constructor
case empty
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
wf_el : ∀ x ∈ 0, Acc LT.lt x
⊢ AccM_1 0
case empty.h
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
wf_el : ∀ x ∈ 0, Acc LT.lt x
⊢ ∀ (y : Multiset α), MultisetRedLt y 0 → Acc MultisetRedLt y