Upstream Bi Interface Changes
To upstream Iris parametric into Iris master, one crucial step will be changing the bi
interface to move out the commuting rules for the later modality and some rules for timelessness.
This change is largely independent of #1 and #2, but requires a "lock" on changing the bi
-interface and the proof mode of Iris.