This class whose name is horrible and purpose is arbitrary seems to be a
leftover of some experiment with ch2o, a long time a ago.

That way type class search becomes more predictable.

Lifting lemmas : make the initial state appear under an existential under the view shift. This is still sound, but slightly more expressive.

This may save the need to seal off some stuff.

New lemma : cmra_update_valid0. This let us prove a FP update using the additionnal hypothesis that the source is valid at step 0.

In particular, it no longer uses set_solver (which made it often slow
or diverge) but a more specific lemma about subseteq.