apply tail
case tail
α β : 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)
⊢ RTC S (f a) (f c)
case tail.hab
α β : 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)
⊢ RTC S (f a) ?tail.b

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 ?tail.b (f c)

case tail.b
α β : 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)
⊢ β