induction h with
| refl =>
  exact refl
| tail b' c _ hb'c ih =>
  apply ih (P := fun a hab' ↦ P a (RTC.tail _ _ hab' hb'c))
  { exact head _ _ hb'c _ refl }
  { intro x y hxy hyb' hy
    exact head _ _ hxy _ hy }
α : Type
R : α → α → Prop
b : α
P : (a : α) → RTC R a b → Prop
a : α
h : RTC R a b
refl : P b (_ : RTC R b b)
head : ∀ (a c : α) (h' : R a c) (h : RTC R c b), P c h → P a (_ : RTC R a b)
⊢ P a h
no goals