WIP: step_proto abstraction

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)