apply mord_wf_1
case intro
α : 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)
⊢ Acc MultisetRedLt (a ::ₘ x)
case intro.x
α : 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)
⊢ Multiset α

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 : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)

case intro.H2
α : 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)
⊢ AccM_1 x

case intro.H3
α : 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)
⊢ ∀ (M : Multiset α), MultisetRedLt M x → AccM_1 (a ::ₘ M)