simp
case assign
s : State
x : String
a : State → ℕ
⊢ (¬∃ T t, (Stmt.assign x a, s) ⇒ (T, t)) ↔ Stmt.assign x a = Stmt.skip
case assign
s : State
x : String
a : State → ℕ
⊢ ∃ T t, (Stmt.assign x a, s) ⇒ (T, t)