apply RTC.single
case assign
Ss : Stmt × State
t : State
x✝ : String
a✝ : State → ℕ
s✝ : State
⊢ RTC SmallStep (Stmt.assign x✝ a✝, s✝) (Stmt.skip, State.update x✝ (a✝ s✝) s✝)
case assign.hab
Ss : Stmt × State
t : State
x✝ : String
a✝ : State → ℕ
s✝ : State
⊢ (Stmt.assign x✝ a✝, s✝) ⇒ (Stmt.skip, State.update x✝ (a✝ s✝) s✝)