intros N N_lt
case h
α : Type u
x✝ : Multiset α
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
M0 : Multiset α
H1 : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
H2 : AccM_1 M0
H3 : ∀ (M : Multiset α), MultisetRedLt M M0 → AccM_1 (a ::ₘ M)
⊢ ∀ (y : Multiset α), MultisetRedLt y (a ::ₘ M0) → Acc MultisetRedLt y
case h
α : Type u
x✝ : Multiset α
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
M0 : Multiset α
H1 : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
H2 : AccM_1 M0
H3 : ∀ (M : Multiset α), MultisetRedLt M M0 → AccM_1 (a ::ₘ M)
N : Multiset α
N_lt : MultisetRedLt N (a ::ₘ M0)
⊢ Acc MultisetRedLt N