case intro
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type ?u.32484
δ : Type ?u.32487
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a a₁ a₂ : α
b✝¹ b₁ b₂ : β
x y : α ⊕ β
aca : ∀ (a : α), Acc (Lex r s) (inl a)
b✝ b : β
h✝ : ∀ (y : β), s y b → Acc s y
IH : ∀ (y : β), s y b → Acc (Lex r s) (inr y)
⊢ Acc (Lex r s) (inr b)
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type ?u.32484
δ : Type ?u.32487
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a a₁ a₂ : α
b✝ b₁ b₂ : β
x y : α ⊕ β
aca : ∀ (a : α), Acc (Lex r s) (inl a)
b : β
acb : Acc s b
⊢ Acc (Lex r s) (inr b)
induction' acb with b _ IH
case intro.h
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type ?u.32484
δ : Type ?u.32487
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a a₁ a₂ : α
b✝¹ b₁ b₂ : β
x y : α ⊕ β
aca : ∀ (a : α), Acc (Lex r s) (inl a)
b✝ b : β
h✝ : ∀ (y : β), s y b → Acc s y
IH : ∀ (y : β), s y b → Acc (Lex r s) (inr y)
⊢ ∀ (y : α ⊕ β), Lex r s y (inr b) → Acc (Lex r s) y
case intro
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type ?u.32484
δ : Type ?u.32487
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a a₁ a₂ : α
b✝¹ b₁ b₂ : β
x y : α ⊕ β
aca : ∀ (a : α), Acc (Lex r s) (inl a)
b✝ b : β
h✝ : ∀ (y : β), s y b → Acc s y
IH : ∀ (y : β), s y b → Acc (Lex r s) (inr y)
⊢ Acc (Lex r s) (inr b)
constructor
case intro.h
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type ?u.32484
δ : Type ?u.32487
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a a₁ a₂ : α
b✝¹ b₁ b₂ : β
x y✝ : α ⊕ β
aca : ∀ (a : α), Acc (Lex r s) (inl a)
b✝ b : β
h✝ : ∀ (y : β), s y b → Acc s y
IH : ∀ (y : β), s y b → Acc (Lex r s) (inr y)
y : α ⊕ β
h : Lex r s y (inr b)
⊢ Acc (Lex r s) y
case intro.h
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type ?u.32484
δ : Type ?u.32487
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a a₁ a₂ : α
b✝¹ b₁ b₂ : β
x y : α ⊕ β
aca : ∀ (a : α), Acc (Lex r s) (inl a)
b✝ b : β
h✝ : ∀ (y : β), s y b → Acc s y
IH : ∀ (y : β), s y b → Acc (Lex r s) (inr y)
⊢ ∀ (y : α ⊕ β), Lex r s y (inr b) → Acc (Lex r s) y
intro y h
case intro.h.inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type ?u.32484
δ : Type ?u.32487
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a a₁ a₂ : α
b✝¹ b₁ b₂ : β
x y : α ⊕ β
aca : ∀ (a : α), Acc (Lex r s) (inl a)
b✝ b : β
h✝ : ∀ (y : β), s y b → Acc s y
IH : ∀ (y : β), s y b → Acc (Lex r s) (inr y)
b' : β
h' : s b' b
⊢ Acc (Lex r s) (inr b')

case intro.h.sep
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type ?u.32484
δ : Type ?u.32487
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a✝ a₁ a₂ : α
b✝¹ b₁ b₂ : β
x y : α ⊕ β
aca : ∀ (a : α), Acc (Lex r s) (inl a)
b✝ b : β
h✝ : ∀ (y : β), s y b → Acc s y
IH : ∀ (y : β), s y b → Acc (Lex r s) (inr y)
a : α
⊢ Acc (Lex r s) (inl a)
case intro.h
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type ?u.32484
δ : Type ?u.32487
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a a₁ a₂ : α
b✝¹ b₁ b₂ : β
x y✝ : α ⊕ β
aca : ∀ (a : α), Acc (Lex r s) (inl a)
b✝ b : β
h✝ : ∀ (y : β), s y b → Acc s y
IH : ∀ (y : β), s y b → Acc (Lex r s) (inr y)
y : α ⊕ β
h : Lex r s y (inr b)
⊢ Acc (Lex r s) y
cases' h with _ _ _ b' _ h' a
no goals
case intro.h.inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type ?u.32484
δ : Type ?u.32487
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a a₁ a₂ : α
b✝¹ b₁ b₂ : β
x y : α ⊕ β
aca : ∀ (a : α), Acc (Lex r s) (inl a)
b✝ b : β
h✝ : ∀ (y : β), s y b → Acc s y
IH : ∀ (y : β), s y b → Acc (Lex r s) (inr y)
b' : β
h' : s b' b
⊢ Acc (Lex r s) (inr b')
exact IH _ h'
no goals
case intro.h.sep
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type ?u.32484
δ : Type ?u.32487
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a✝ a₁ a₂ : α
b✝¹ b₁ b₂ : β
x y : α ⊕ β
aca : ∀ (a : α), Acc (Lex r s) (inl a)
b✝ b : β
h✝ : ∀ (y : β), s y b → Acc s y
IH : ∀ (y : β), s y b → Acc (Lex r s) (inr y)
a : α
⊢ Acc (Lex r s) (inl a)
exact aca _