This merge request hides the multiple laters that arise from using the Actris Ghost Theory, via a "step-taking" modality |~~> P,
that captures the obligation to take a step of the operational semantics.
One motivation for this is being able to present the abstraction in a way that requires less explanation.
The MR depends on the following outstanding MR of the Iris development iris!887 (closed)