Also update wrt recent iris.

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.

Other changes:
- Get rid of * spec pattern (deprecated in iris trunk)
- Make freeable_sz opaque (and simplifiy some proofs because of this)
- Refact option_as_mut and cell
- Prove lft_glb_acc, for gettings tokens of an intersections from tokens of its components
- Add some support for the = operator for ints in the proof mode

Boxes for function types are part of the function type itself and we do not need to add them everywhere.

This reverts commit 04386c1c.