persistent context.

Given the source does not contain a box:

- Before: no-op if there is a Persistent instance.
- Now: no-op in all cases.

We now first iPoseProof the lemma and instantiate its premises before trying
to search for the sub-term where to apply. As a result, instantiation of the
premises of the applied lemmas happens only once, instead of it being done for
each sub-term as obtained by reshape_expr.

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

Implement greatest fixed point inside the logic

See merge request !60

Fixes #96

Refactor the resources for ticket lock

See merge request !55

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

get rid of the empty-unicode-space hacks

See merge request !59

This makes it easier to frame or introduce some modalities before introducing
universal quantifiers.

That way, we can use Contractive as part of structure definitions in
which we do not have a bundled OFE yet.