apply Exists.intro (s[x ↦ a s])
case assign
s : State
x : String
a : State → ℕ
⊢ ∃ t, (Stmt.assign x a, s) ⇒ (Stmt.skip, t)
case assign
s : State
x : String
a : State → ℕ
⊢ (Stmt.assign x a, s) ⇒ (Stmt.skip, State.update x (a s) s)