huge commit regarding universes:

huge commit regarding universes:
- only Type[foo] can be declare with a strict (<) constraint among other
  Type[bar]
- CProp[foo] is automatically available for Type[foo]
- The CProp hierarchy can be collapsed (hopefully in a consistent way)
  to both Prop OR Type:
  - You cannot eliminate CProp to build a Type like for Prop/Type
  - You cannot eliminate Prop to build a CProp, like for Prop/Type
- Peculiarity: CProp[i] has type Type[i+1], since CProp[i+1] is only >=
  of CProp[i] to allow collapsing them (while < whould be violated).

New function to delift a type w.r.t. a term list, to potentially build a
dependent type, used in lambda_intro and Letin expected type propagation.