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