The intropattern {H} also meant clear (both in ssreflect, and the logic
part of the introduction pattern).

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.