cases hr with
| assign _ _ _ => rfl
case assign
Ss Ll : Stmt × State
x : String
a : State → ℕ
s : State
Rr : Stmt × State
hr : (Stmt.assign x a, s) ⇒ Rr
⊢ (Stmt.skip, State.update x (a s) s) = Rr
no goals