In order to do that, we need to quantify over non-expansive
predicates instead of arbitrary predicates.

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]).

- Use Φ and Ψ for predicates.
- Use _1 and _2 suffixes for the different directions of a lemma.
- Not all lemmas started with _uPred; we do not let the bigop lemmas (for instance)
  start with uPred_ either, so I just got rid of the prefix.

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