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 :/

Fixpoint type. There are still a few TODO for the non-expansiveness of sums, products and functions.