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.
bi
This issue only really makes sense once #1, #2, and #3 are done.