assumption
case mk.mk.hS
S✝ T : Stmt
s✝ u : State
h : RTC SmallStep (S✝, s✝) (Stmt.skip, u)
S : Stmt
s : State
S' : Stmt
s' : State
hrtc : (S, s) ⇒ (S', s')
⊢ ((S, s).fst, (S, s).snd) ⇒ ((S', s').fst, (S', s').snd)
no goals