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.