case refl
α : Type u_1
β : Type ?u.18673
γ : Type ?u.18676
δ : Type ?u.18679
r : α → α → Prop
a b c d : α
hab : TransGen r a b
⊢ TransGen r a b

case tail
α : Type u_1
β : Type ?u.18673
γ : Type ?u.18676
δ : Type ?u.18679
r : α → α → Prop
a b c d : α
hab : TransGen r a b
b✝ c✝ : α
a✝¹ : ReflTransGen r b b✝
a✝ : r b✝ c✝
a_ih✝ : TransGen r a b✝
⊢ TransGen r a c✝
α : Type u_1
β : Type ?u.18673
γ : Type ?u.18676
δ : Type ?u.18679
r : α → α → Prop
a b c d : α
hab : TransGen r a b
hbc : ReflTransGen r b c
⊢ TransGen r a c
induction hbc
case tail
α : Type u_1
β : Type ?u.18673
γ : Type ?u.18676
δ : Type ?u.18679
r : α → α → Prop
a b c d : α
hab : TransGen r a b
b✝ c✝ : α
a✝¹ : ReflTransGen r b b✝
a✝ : r b✝ c✝
a_ih✝ : TransGen r a b✝
⊢ TransGen r a c✝
case refl
α : Type u_1
β : Type ?u.18673
γ : Type ?u.18676
δ : Type ?u.18679
r : α → α → Prop
a b c d : α
hab : TransGen r a b
⊢ TransGen r a b

case tail
α : Type u_1
β : Type ?u.18673
γ : Type ?u.18676
δ : Type ?u.18679
r : α → α → Prop
a b c d : α
hab : TransGen r a b
b✝ c✝ : α
a✝¹ : ReflTransGen r b b✝
a✝ : r b✝ c✝
a_ih✝ : TransGen r a b✝
⊢ TransGen r a c✝
case refl => assumption
no goals
case tail
α : Type u_1
β : Type ?u.18673
γ : Type ?u.18676
δ : Type ?u.18679
r : α → α → Prop
a b c d : α
hab : TransGen r a b
b✝ c✝ : α
a✝¹ : ReflTransGen r b b✝
a✝ : r b✝ c✝
a_ih✝ : TransGen r a b✝
⊢ TransGen r a c✝
case tail c d _ hcd hac => exact hac.tail hcd
no goals
α : Type u_1
β : Type ?u.18673
γ : Type ?u.18676
δ : Type ?u.18679
r : α → α → Prop
a b c d : α
hab : TransGen r a b
⊢ TransGen r a b
assumption
no goals
α : Type u_1
β : Type ?u.18673
γ : Type ?u.18676
δ : Type ?u.18679
r : α → α → Prop
a b c✝ d✝ : α
hab : TransGen r a b
c d : α
a✝ : ReflTransGen r b c
hcd : r c d
hac : TransGen r a c
⊢ TransGen r a d
exact hac.tail hcd