case refl
α : Type u_1
β : Type ?u.26665
γ : Type ?u.26668
δ : Type ?u.26671
r : α → α → Prop
a b c d : α
⊢ ReflTransGen (Function.swap r) b b

case tail
α : Type u_1
β : Type ?u.26665
γ : Type ?u.26668
δ : Type ?u.26671
r : α → α → Prop
a b✝ c✝ d b c : α
a✝ : ReflTransGen r b✝ b
hbc : r b c
ih : ReflTransGen (Function.swap r) b b✝
⊢ ReflTransGen (Function.swap r) c b✝
α : Type u_1
β : Type ?u.26665
γ : Type ?u.26668
δ : Type ?u.26671
r : α → α → Prop
a b c d : α
h : ReflTransGen r b a
⊢ ReflTransGen (Function.swap r) a b
induction' h with b c _ hbc ih
no goals
case refl
α : Type u_1
β : Type ?u.26665
γ : Type ?u.26668
δ : Type ?u.26671
r : α → α → Prop
a b c d : α
⊢ ReflTransGen (Function.swap r) b b
rfl
no goals
case tail
α : Type u_1
β : Type ?u.26665
γ : Type ?u.26668
δ : Type ?u.26671
r : α → α → Prop
a b✝ c✝ d b c : α
a✝ : ReflTransGen r b✝ b
hbc : r b c
ih : ReflTransGen (Function.swap r) b b✝
⊢ ReflTransGen (Function.swap r) c b✝
exact ih.head hbc