case refl
α : Type u_1
β : Type ?u.25222
γ : Type ?u.25225
δ : Type ?u.25228
r : α → α → Prop
a✝ b✝ c d : α
refl : Reflexive r
trans : Transitive r
a b : α
⊢ r a a

case tail
α : Type u_1
β : Type ?u.25222
γ : Type ?u.25225
δ : Type ?u.25228
r : α → α → Prop
a✝¹ b✝¹ c✝ d : α
refl : Reflexive r
trans : Transitive r
a b✝ b c : α
a✝ : ReflTransGen r a b
h₂ : r b c
IH : r a b
⊢ r a c
α : Type u_1
β : Type ?u.25222
γ : Type ?u.25225
δ : Type ?u.25228
r : α → α → Prop
a✝ b✝ c d : α
refl : Reflexive r
trans : Transitive r
a b : α
h : ReflTransGen r a b
⊢ r a b
induction' h with b c _ h₂ IH
no goals
case refl
α : Type u_1
β : Type ?u.25222
γ : Type ?u.25225
δ : Type ?u.25228
r : α → α → Prop
a✝ b✝ c d : α
refl : Reflexive r
trans : Transitive r
a b : α
⊢ r a a
apply refl
no goals
case tail
α : Type u_1
β : Type ?u.25222
γ : Type ?u.25225
δ : Type ?u.25228
r : α → α → Prop
a✝¹ b✝¹ c✝ d : α
refl : Reflexive r
trans : Transitive r
a b✝ b c : α
a✝ : ReflTransGen r a b
h₂ : r b c
IH : r a b
⊢ r a c
exact trans IH h₂