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

update stdpp

See merge request FP/iris-coq!68

This causes a bit of backwards incompatibility: it may now succeed with
later stripping below unlocked/TC transparent definitions. This problem
actually occured for `wsat`.

Common tactic machinery for symbolic execution of pure reductions

See merge request FP/iris-coq!64

We used to normalize the goal, and then checked whether it was of
a certain shape. Since `uPred_valid P` normalized to `True ⊢ P`,
there was no way of making a distinction between the two, hence
`True ⊢ P` was treated as `uPred_valid P`.

In this commit, I use type classes to check whether the goal is of
a certain shape. Since we declared `uPred_valid` as `Typeclasses
Opaque`, we can now make a distinction between `True ⊢ P` and
`uPred_valid P`.