]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/re_complete/basics/pts.ma
update in ground
[helm.git] / matita / matita / re_complete / basics / pts.ma
1 include "basics/core_notation.ma".
2
3 universe constraint Type[0] < Type[1].
4 universe constraint Type[1] < Type[2].
5 universe constraint Type[2] < Type[3].
6 universe constraint Type[3] < Type[4].
7 universe constraint Type[4] < Type[5].