That caused some problems, e.g.:

  From iris.base_logic Require Export fix.

Gave:

  Syntax error: [constr:global] expected after
  [export_token] (in [vernac:gallina_ext]).

Implementation is by Robbert <FP/iris-atomic!5 (comment 19496)>

Instead, I have introduced a type class `Monoid` that is used by the big operators:

    Class Monoid {M : ofeT} (o : M → M → M) := {
      monoid_unit : M;
      monoid_ne : NonExpansive2 o;
      monoid_assoc : Assoc (≡) o;
      monoid_comm : Comm (≡) o;
      monoid_left_id : LeftId (≡) monoid_unit o;
      monoid_right_id : RightId (≡) monoid_unit o;
    }.

Note that the operation is an argument because we want to have multiple monoids over
the same type (for example, on `uPred`s we have monoids for `∗`, `∧`, and `∨`). However,
we do bundle the unit because:

- If we would not, the unit would appear explicitly in an implicit argument of the
  big operators, which confuses rewrite. By bundling the unit in the `Monoid` class
  it is hidden, and hence rewrite won't even see it.
- The unit is unique.

We could in principle have big ops over setoids instead of OFEs. However, since we do
not have a canonical structure for bundled setoids, I did not go that way.

Also:

- Remove the wp_strip_later hack.
- Let wp_lam, wp_rec, wp_... initiate the proof mode.

Really, *all* of our files contain proof rules

Thanks to Robbert for fixing gen_heap

Use COFEs only for the recursive domain equation solver

This way we avoid the env_cbv tactic unfolding string related stuff
that appears in the goal and hypotheses of the proof mode.

And also rename the corresponding proof mode tactics.

rename program_logic.{ownership -> wsat}. It really is about world satisfaction and invariants more than about ownership.

Used in iRevert, iClear, iFrame, and for generalizing the IH in
iInduction and iLöb.