cases Ss' with
| mk S' s' =>
  apply BigStep_of_SmallStep_of_BigStep hST
  apply ih
case head
Ss✝ : Stmt × State
t : State
Ss Ss' : Stmt × State
hST : Ss ⇒ Ss'
hsmallT : RTC SmallStep Ss' (Stmt.skip, t)
ih : Ss' ⟹ t
⊢ Ss ⟹ t
no goals