Upstream Parametric Algebra
To upstream Iris parametric into Iris master, one crucial step will be updating the algebra folder to use a generic definition of OFEs, COFEs, and CMRAs. To avoid this change from growing too large, the bi
interface and the base logic should be defined in terms of a natural number step-index. This way, we do not have to change the rules of the proof mode and its type classes just yet.
This change can be prepared concurrently to #1. It does, however, overlap with this issue, because dist_later
is defined in the algebra folder.