New notation for product type. Only functions can be generalized. Fix perm_incl_share by adding tokens.

Main changes:

- Use new notion of local updates.
- Use new big operators over CMRAs.
- Factor out common properties of lrust in heap.

Rename bot into emp. Revert a wrong simplification of the previous commit (emp has to be defined manually).

Inclusion of permissions. In order to make type inclusion working, I had to change the inclusion of types also.

I also had to change the definition of simple types, so that shared borrows are monotonous wrt. their lifetime.
Also, reorganization of the files.

The problem with forall is that a duplicable assertion is not necessarilly duplicable after being generalized.

Also simplified the interface of lifetimes by currying them.

Unique borrows. \n\n Actually, there is still an admit, I'm not sure its provable using the current lifetime logic.