cases Ss' with
| mk S' s' =>
  apply SmallStep.seq_step
  assumption
case mk
S✝ T : Stmt
s✝ u : State
h : RTC SmallStep (S✝, s✝) (Stmt.skip, u)
Ss' : Stmt × State
S : Stmt
s : State
hrtc : (S, s) ⇒ Ss'
⊢ (fun Ss => (Ss.fst; T, Ss.snd)) (S, s) ⇒ (fun Ss => (Ss.fst; T, Ss.snd)) Ss'
no goals