(Im)mutable borrowing of refcells.

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