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.

This reverts commit 04386c1c.

For consistency with how we call this elsewhere in Iris.

Typechecked lazy lifetime initialization. Also, switched from eauto to typeclasses eauto, which seems way less bugged (but I still found something strange...).

Coq's module system is wholly inadequate :/