rw [heq]
case mpr
x : String
a : State → ℕ
s t : State
heq : t = State.update x (a s) s
⊢ (Stmt.assign x a, s) ⟹ t
case mpr
x : String
a : State → ℕ
s t : State
heq : t = State.update x (a s) s
⊢ (Stmt.assign x a, s) ⟹ State.update x (a s) s