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.