From e9eda8f13045ff3d4f7b1ec93dec96e09bf65f1a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 8 Jul 2009 09:58:29 +0000
Subject: [PATCH] removed useless universes

---
 helm/software/matita/tests/esempio_oliboni.ma | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

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
+  
-- 
2.39.2