Make box a definition and prove it contractive

See merge request !5

Fix [solve__typing] by changing the hint on [tctx_extract_hasty_here_eq] into a [Hint Resolve], so that the opaqueness annotations are not ignored.

This also allows us to get rid of ctx_eq

This simplifies the statements of all the toplevel typing theorem, and make them generic on the lifetime contexts, so that they can actually be used.

make the metric on types the expected one; define the old metric as another relation that's used only for constructing the fixpoint

This makes us able to have a smaller mask for ending a lifetime, and hence we get rid of an admit in RwLock.

FIXME : we need to be able to end a lifetime when an invariant is still open.

This requires using a different invariant in the case N ⊥ lftN. Hence, we add the side condition that (N = lftN ∨ N ⊥ lftN). This is not particularly pretty : the alternative would be to have two different kinds of shared borrows.

* Also, removed the box from the definition of typing judgments, so that we can frame resources around them.

This requires using iApply instead of eapply to use them.

TODO : have an Iris version of Forall2, so that the lemmas for typing switches can be implications in Iris.