case single
α : Type u_1
β : Type ?u.23725
γ : Type ?u.23728
δ : Type ?u.23731
r : α → α → Prop
a b✝ c d b : α
h : r b✝ b
⊢ TransGen (Function.swap r) b b✝

case tail
α : Type u_1
β : Type ?u.23725
γ : Type ?u.23728
δ : Type ?u.23731
r : α → α → Prop
a b✝ c✝ d b c : α
a✝ : TransGen r b✝ b
hbc : r b c
ih : TransGen (Function.swap r) b b✝
⊢ TransGen (Function.swap r) c b✝
α : Type u_1
β : Type ?u.23725
γ : Type ?u.23728
δ : Type ?u.23731
r : α → α → Prop
a b c d : α
h : TransGen r b a
⊢ TransGen (Function.swap r) a b
induction' h with b h b c _ hbc ih
no goals
case single
α : Type u_1
β : Type ?u.23725
γ : Type ?u.23728
δ : Type ?u.23731
r : α → α → Prop
a b✝ c d b : α
h : r b✝ b
⊢ TransGen (Function.swap r) b b✝
exact TransGen.single h
no goals
case tail
α : Type u_1
β : Type ?u.23725
γ : Type ?u.23728
δ : Type ?u.23731
r : α → α → Prop
a b✝ c✝ d b c : α
a✝ : TransGen r b✝ b
hbc : r b c
ih : TransGen (Function.swap r) b b✝
⊢ TransGen (Function.swap r) c b✝
exact ih.head hbc