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