stateAssert is currently used within the design spec to assert properties about the state. However, given that we do not translate the string associated with the Haskell assert into the design spec, our use of stateAssert offers no benefit over state_assert.

We should investigate replacing stateAssert with state_assert, which would require a change to the Haskell translator.

Alternatives include

• having a global simp that turns stateAssert into state_assert and rewriting our corres_underlying/ccorres_underlying rules in terms of state_assert, or

• providing lemmas statements for our existing corres_underlying/ccorres_underlying rules to use state_assert instead of stateAssert, for example ccorres_stateAssert[simplified stateAssert_def] or similar