case single
α : Type u_1
β : Type ?u.18514
γ : Type ?u.18517
δ : Type ?u.18520
r : α → α → Prop
a✝ b✝¹ c d a b✝ b : α
h : r a b
⊢ ReflTransGen r a b

case tail
α : Type u_1
β : Type ?u.18514
γ : Type ?u.18517
δ : Type ?u.18520
r : α → α → Prop
a✝¹ b✝¹ c✝ d a b✝ b c : α
a✝ : TransGen r a b
bc : r b c
ab : ReflTransGen r a b
⊢ ReflTransGen r a c
α : Type u_1
β : Type ?u.18514
γ : Type ?u.18517
δ : Type ?u.18520
r : α → α → Prop
a✝ b✝ c d a b : α
h : TransGen r a b
⊢ ReflTransGen r a b
induction' h with b h b c _ bc ab
case tail
α : Type u_1
β : Type ?u.18514
γ : Type ?u.18517
δ : Type ?u.18520
r : α → α → Prop
a✝¹ b✝¹ c✝ d a b✝ b c : α
a✝ : TransGen r a b
bc : r b c
ab : ReflTransGen r a b
⊢ ReflTransGen r a c
case single
α : Type u_1
β : Type ?u.18514
γ : Type ?u.18517
δ : Type ?u.18520
r : α → α → Prop
a✝ b✝¹ c d a b✝ b : α
h : r a b
⊢ ReflTransGen r a b

case tail
α : Type u_1
β : Type ?u.18514
γ : Type ?u.18517
δ : Type ?u.18520
r : α → α → Prop
a✝¹ b✝¹ c✝ d a b✝ b c : α
a✝ : TransGen r a b
bc : r b c
ab : ReflTransGen r a b
⊢ ReflTransGen r a c
exact ReflTransGen.single h
no goals
case tail
α : Type u_1
β : Type ?u.18514
γ : Type ?u.18517
δ : Type ?u.18520
r : α → α → Prop
a✝¹ b✝¹ c✝ d a b✝ b c : α
a✝ : TransGen r a b
bc : r b c
ab : ReflTransGen r a b
⊢ ReflTransGen r a c
exact ReflTransGen.tail ab bc