unfold AccM_1
case intro.H1
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a✝ : α
H : ∀ (b : α) (M : Multiset α), b < a✝ → AccM_1 M → AccM_1 (b ::ₘ M)
M x✝ : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x✝ → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x✝ → Acc MultisetRedLt (a✝ ::ₘ y)
b : α
x : Multiset α
a : b < a✝
⊢ AccM_1 x → AccM_1 (b ::ₘ x)
case intro.H1
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a✝ : α
H : ∀ (b : α) (M : Multiset α), b < a✝ → AccM_1 M → AccM_1 (b ::ₘ M)
M x✝ : Multiset α
wfH : ∀ (y : Multiset α), MultisetRedLt y x✝ → Acc MultisetRedLt y
wfH2 : ∀ (y : Multiset α), MultisetRedLt y x✝ → Acc MultisetRedLt (a✝ ::ₘ y)
b : α
x : Multiset α
a : b < a✝
⊢ Acc MultisetRedLt x → Acc MultisetRedLt (b ::ₘ x)