+let _ =
+let mk_type n =
+ if n = 0 then
+ [false, NUri.uri_of_string ("cic:/matita/pts/Type.univ")]
+ else
+ [false, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".univ")]
+in
+let mk_cprop n =
+ if n = 0 then
+ [false, NUri.uri_of_string ("cic:/matita/pts/CProp.univ")]
+ else
+ [false, NUri.uri_of_string ("cic:/matita/pts/CProp"^string_of_int n^".univ")]
+in
+ NCicEnvironment.add_constraint true (mk_type 0) (mk_type 1);
+ NCicEnvironment.add_constraint true (mk_cprop 0) (mk_cprop 1);
+ NCicEnvironment.add_constraint true (mk_cprop 0) (mk_type 1);
+ NCicEnvironment.add_constraint true (mk_type 0) (mk_cprop 1);
+ NCicEnvironment.add_constraint false (mk_cprop 0) (mk_type 0);
+ NCicEnvironment.add_constraint false (mk_type 0) (mk_cprop 0);
+
+ NCicEnvironment.add_constraint true (mk_type 1) (mk_type 2);
+ NCicEnvironment.add_constraint true (mk_cprop 1) (mk_cprop 2);
+ NCicEnvironment.add_constraint true (mk_cprop 1) (mk_type 2);
+ NCicEnvironment.add_constraint true (mk_type 1) (mk_cprop 2);
+ NCicEnvironment.add_constraint false (mk_cprop 1) (mk_type 1);
+ NCicEnvironment.add_constraint false (mk_type 1) (mk_cprop 1);
+
+ NCicEnvironment.add_constraint true (mk_type 2) (mk_type 3);
+ NCicEnvironment.add_constraint true (mk_cprop 2) (mk_cprop 3);
+ NCicEnvironment.add_constraint true (mk_cprop 2) (mk_type 3);
+ NCicEnvironment.add_constraint true (mk_type 2) (mk_cprop 3);
+ NCicEnvironment.add_constraint false (mk_cprop 2) (mk_type 2);
+ NCicEnvironment.add_constraint false (mk_type 2) (mk_cprop 2);
+
+ NCicEnvironment.add_constraint false (mk_cprop 3) (mk_type 3);
+ NCicEnvironment.add_constraint false (mk_type 3) (mk_cprop 3);
+
+;;
+