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.