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`.

Use `ε` for CMRA unit

See merge request !62

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

For obsolete reasons, that no longer seem to apply, we used ∅ as the
unit.

Fix typo in is_lock_proper for heap_lang.

See merge request !57