removed useless universes

diff --git a/helm/software/matita/tests/esempio_oliboni.ma b/helm/software/matita/tests/esempio_oliboni.ma
index aca01514d6559b3035c9ec788d2c42eebd684f92..8eb612e4e7d1239ce19c9676e4d4dbfb61278885 100644 (file)
--- a/helm/software/matita/tests/esempio_oliboni.ma
+++ b/helm/software/matita/tests/esempio_oliboni.ma
@@ -18,13 +18,10 @@ include "nat/nat.ma".
 universe constraint Type[0] < Type[1].
 universe constraint Type[1] < Type[2].
 universe constraint CProp[0] < CProp[1].
-universe constraint CProp[1] < CProp[2].
 universe constraint Type[0] ≤ CProp[0].
 universe constraint CProp[0] ≤ Type[0].
 universe constraint Type[1] ≤ CProp[1].
 universe constraint CProp[1] ≤ Type[1].
-universe constraint Type[2] ≤ CProp[2].
-universe constraint CProp[2] ≤ Type[2].
 
 ninductive A : Type[0] ≝ 
  | K : nat → A
@@ -62,4 +59,4 @@ ncases a; ncases b;
 
 
 
-  
\ No newline at end of file
+