X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Ftests%2Fesempio_oliboni.ma;h=8eb612e4e7d1239ce19c9676e4d4dbfb61278885;hb=e9eda8f13045ff3d4f7b1ec93dec96e09bf65f1a;hp=aca01514d6559b3035c9ec788d2c42eebd684f92;hpb=60a2463fd555462e159c84a38b62b1b621bb10e6;p=helm.git

diff --git a/helm/software/matita/tests/esempio_oliboni.ma b/helm/software/matita/tests/esempio_oliboni.ma
index aca01514d..8eb612e4e 100644
--- 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
+