The common principle is "unnesting an index borrow". This simplifies
the proofs of reborrowing and unnesting, and, moreover, gives a slightly
stronger unnesting rule (the masks are different).

Begining the work on weak references in Rc: redesign the protocol, define the weak type, and update the code for rc.

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

The interface is slightly more flexible than the one on iris.heap_lang to support continuation passing style

Also : declared a canonical structure for lft as a leibniz ofe, and changed the statement of wp_memcpy, so that it unifys with any relevant goal.