Theorem: LoVe.RTC.RTC_RTC_eq (LoVe/LoVelib.lean)

State before:
α : Type
R : α → α → Prop
a b : α
h : RTC (RTC R) a b
⊢ RTC R a b
Tactic:
induction h with
| refl => exact refl
| tail b c hab' hbc ih =>
  apply trans <;>
    assumption
State after:
no goals

State before:
case refl
α : Type
R : α → α → Prop
a b : α
⊢ RTC R a a
Tactic:
exact refl
State after:
no goals

State before:
case tail
α : Type
R : α → α → Prop
a b✝ b c : α
hab' : RTC (RTC R) a b
hbc : RTC R b c
ih : RTC R a b
⊢ RTC R a c
Tactic:
apply trans <;>
  assumption
State after:
no goals