This way, we do not have to duplicate a lot of theory, and we made sure
that we have all lemmas/class instances for both modalities.

Now that we have the plain modality, we can get rid of the basic updates
in the soundness statement.

Introduce a connective `ilocked` to stop `iNext` and `iFrame`.

See merge request FP/iris-coq!67

use primitive projections for our mixins

See merge request FP/iris-coq!69

Remove an unused argument for `newcounter_mono_spec`.

See merge request FP/iris-coq!70