induction hab with
| refl => apply refl
| tail b c hab hbc ih =>
  apply tail
  apply ih
  apply hf
  exact hbc
α β : Type
R : α → α → Prop
S : β → β → Prop
a b : α
f : α → β
hf : ∀ (a b : α), R a b → S (f a) (f b)
hab : RTC R a b
⊢ RTC S (f a) (f b)
no goals