case refl
α : Type u_1
β : Type ?u.19655
γ : Type ?u.19658
δ : Type ?u.19661
r : α → α → Prop
a b d c : α
hbc : r a c
⊢ TransGen r a c

case tail
α : Type u_1
β : Type ?u.19655
γ : Type ?u.19658
δ : Type ?u.19661
r : α → α → Prop
a b d b✝ c✝ : α
a✝¹ : ReflTransGen r a b✝
a✝ : r b✝ c✝
a_ih✝ : ∀ {c : α}, r b✝ c → TransGen r a c
c : α
hbc : r c✝ c
⊢ TransGen r a c
α : Type u_1
β : Type ?u.19655
γ : Type ?u.19658
δ : Type ?u.19661
r : α → α → Prop
a b c d : α
hab : ReflTransGen r a b
hbc : r b c
⊢ TransGen r a c
induction hab generalizing c
case tail
α : Type u_1
β : Type ?u.19655
γ : Type ?u.19658
δ : Type ?u.19661
r : α → α → Prop
a b d b✝ c✝ : α
a✝¹ : ReflTransGen r a b✝
a✝ : r b✝ c✝
a_ih✝ : ∀ {c : α}, r b✝ c → TransGen r a c
c : α
hbc : r c✝ c
⊢ TransGen r a c
case refl
α : Type u_1
β : Type ?u.19655
γ : Type ?u.19658
δ : Type ?u.19661
r : α → α → Prop
a b d c : α
hbc : r a c
⊢ TransGen r a c

case tail
α : Type u_1
β : Type ?u.19655
γ : Type ?u.19658
δ : Type ?u.19661
r : α → α → Prop
a b d b✝ c✝ : α
a✝¹ : ReflTransGen r a b✝
a✝ : r b✝ c✝
a_ih✝ : ∀ {c : α}, r b✝ c → TransGen r a c
c : α
hbc : r c✝ c
⊢ TransGen r a c
case refl => exact single hbc
no goals
case tail
α : Type u_1
β : Type ?u.19655
γ : Type ?u.19658
δ : Type ?u.19661
r : α → α → Prop
a b d b✝ c✝ : α
a✝¹ : ReflTransGen r a b✝
a✝ : r b✝ c✝
a_ih✝ : ∀ {c : α}, r b✝ c → TransGen r a c
c : α
hbc : r c✝ c
⊢ TransGen r a c
case tail _ _ _ hdb IH => exact tail (IH hdb) hbc
no goals
α : Type u_1
β : Type ?u.19655
γ : Type ?u.19658
δ : Type ?u.19661
r : α → α → Prop
a b d c : α
hbc : r a c
⊢ TransGen r a c
exact single hbc
no goals
α : Type u_1
β : Type ?u.19655
γ : Type ?u.19658
δ : Type ?u.19661
r : α → α → Prop
a b d b✝ c✝ : α
a✝ : ReflTransGen r a b✝
hdb : r b✝ c✝
IH : ∀ {c : α}, r b✝ c → TransGen r a c
c : α
hbc : r c✝ c
⊢ TransGen r a c
exact tail (IH hdb) hbc