apply hf
case tail.hbc
α β : Type
R : α → α → Prop
S : β → β → Prop
a b✝ : α
f : α → β
hf : ∀ (a b : α), R a b → S (f a) (f b)
b c : α
hab : RTC R a b
hbc : R b c
ih : RTC S (f a) (f b)
⊢ S (f b) (f c)
case tail.hbc.a
α β : Type
R : α → α → Prop
S : β → β → Prop
a b✝ : α
f : α → β
hf : ∀ (a b : α), R a b → S (f a) (f b)
b c : α
hab : RTC R a b
hbc : R b c
ih : RTC S (f a) (f b)
⊢ R b c