Fixpoint type. There are still a few TODO for the non-expansiveness of sums, products and functions.

Also, to fix the build: use compatibility layer for ownP.
TODO : connect the heap invariant directly.

Refactoring the type system : every type gets its own file. Some trivial ones are defined somewhere else where it make the most sense.

Also, perform some refactoring.

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.

   + Put laters around heap assumptions in heap.v
- A few fixes in substitutions.v :
   + Replaced csimpl by cbn [subst_l subst'] in simpl_subst for
     better performances
   + Enforce the right order for rewriting do_subst
   + added list constructors instances for WSubstL
   + Fixed the hint extern for WSubst Rec
- Compatibility with new intro patterns
- Better notations for language constructs : function parameters are
  listed within []
- Proved memcpy. TODO : improve perforamnces (time and memory).