induction hS using RTC.head_induction_on with
| refl =>
  apply BigStep.skip
| head Ss Ss' hST hsmallT ih =>
  cases Ss' with
  | mk S' s' =>
    apply BigStep_of_SmallStep_of_BigStep hST
    apply ih
Ss : Stmt × State
t : State
hS : RTC SmallStep Ss (Stmt.skip, t)
⊢ Ss ⟹ t
no goals