Upstream Parametric BI and Proofmode
To upstream Iris parametric into Iris master, one crucial step will be making the bi
-interface and the Iris proof mode parametric over the step-index.
This issue only really makes sense once #1, #2, and #3 are done.