case intro
α : Type u_1
β : Type ?u.22046
γ : Type ?u.22049
δ : Type ?u.22052
r : α → α → Prop
a b c d x : α
h✝ : ∀ (y : α), r y x → Acc r y
H : ∀ (y : α), r y x → Acc (Relation.TransGen r) y
⊢ Acc (Relation.TransGen r) x
α : Type u_1
β : Type ?u.22046
γ : Type ?u.22049
δ : Type ?u.22052
r : α → α → Prop
a b c d : α
h : Acc r a
⊢ Acc (Relation.TransGen r) a
induction' h with x _ H
case intro
α : Type u_1
β : Type ?u.22046
γ : Type ?u.22049
δ : Type ?u.22052
r : α → α → Prop
a b c d x : α
h✝ : ∀ (y : α), r y x → Acc r y
H : ∀ (y : α), r y x → Acc (Relation.TransGen r) y
y : α
hy : Relation.TransGen r y x
⊢ Acc (Relation.TransGen r) y
case intro
α : Type u_1
β : Type ?u.22046
γ : Type ?u.22049
δ : Type ?u.22052
r : α → α → Prop
a b c d x : α
h✝ : ∀ (y : α), r y x → Acc r y
H : ∀ (y : α), r y x → Acc (Relation.TransGen r) y
⊢ Acc (Relation.TransGen r) x
refine' Acc.intro x fun y hy ↦ _
case intro.single
α : Type u_1
β : Type ?u.22046
γ : Type ?u.22049
δ : Type ?u.22052
r : α → α → Prop
a b c d x : α
h✝ : ∀ (y : α), r y x → Acc r y
H : ∀ (y : α), r y x → Acc (Relation.TransGen r) y
y : α
hyx : r y x
⊢ Acc (Relation.TransGen r) y

case intro.tail
α : Type u_1
β : Type ?u.22046
γ : Type ?u.22049
δ : Type ?u.22052
r : α → α → Prop
a b c d x : α
h✝ : ∀ (y : α), r y x → Acc r y
H : ∀ (y : α), r y x → Acc (Relation.TransGen r) y
y z : α
hyz : Relation.TransGen r y z
hzx : r z x
⊢ Acc (Relation.TransGen r) y
case intro
α : Type u_1
β : Type ?u.22046
γ : Type ?u.22049
δ : Type ?u.22052
r : α → α → Prop
a b c d x : α
h✝ : ∀ (y : α), r y x → Acc r y
H : ∀ (y : α), r y x → Acc (Relation.TransGen r) y
y : α
hy : Relation.TransGen r y x
⊢ Acc (Relation.TransGen r) y
cases' hy with _ hyx z _ hyz hzx
no goals
case intro.single
α : Type u_1
β : Type ?u.22046
γ : Type ?u.22049
δ : Type ?u.22052
r : α → α → Prop
a b c d x : α
h✝ : ∀ (y : α), r y x → Acc r y
H : ∀ (y : α), r y x → Acc (Relation.TransGen r) y
y : α
hyx : r y x
⊢ Acc (Relation.TransGen r) y

case intro.tail
α : Type u_1
β : Type ?u.22046
γ : Type ?u.22049
δ : Type ?u.22052
r : α → α → Prop
a b c d x : α
h✝ : ∀ (y : α), r y x → Acc r y
H : ∀ (y : α), r y x → Acc (Relation.TransGen r) y
y z : α
hyz : Relation.TransGen r y z
hzx : r z x
⊢ Acc (Relation.TransGen r) y
exacts [H y hyx, (H z hzx).inv hyz]