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.