That way type class search becomes more predictable.

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.

In noticed in Amin's development that importing the proof mode often
turns length into String.length. The weird thing is that before importing
the proof mode, it refers to List.length, and when importing just the
proof mode, it refers to List.length too. However, in some combinations of
imports, it seems to result in it refering to String.length...

For example iIntros "{$H1 H2} H1" frames H1, clears H2, and introduces H1.

I know we don't use it.  Stating theorems also serves to document things, and IMHO this one is informative.  It also costs us nothing.

This fixes a bug in 916ff44a causing proof mode notations not being
pretty printed.

Concretely, when execution of any of the wp_ tactics does not yield
another wp, it will make sure that a view shift is kept. This
behavior was already partially there, but now it is hopefully more
consistent.

This tweak allows us to declare pvs as an instance of FromPure (it is not
an instance of IntoPure), making some tactics (like iPureIntro and done)
work with pvs too.