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