## Summary Port the remaining items from [`base_logic/proofmode.v`](https://gitlab.mpi-sws.org/iris/iris/-/blob/master/iris/base_logic/proofmode.v). ## Subtasks - [ ] Class instances ## Dependencies **Rocq dependencies:** - #229 - #293 - #219
Summary
Port the remaining items from
base_logic/proofmode.v.Subtasks
Dependencies
Rocq dependencies: