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.