X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Ftopology%2Figft.ma;h=d6043fba2c1d413fc22626fd567e18dbc34c5779;hb=a8285ad2e16e571100a666bc9178347d9e61dbe5;hp=3c0ba7090406c43aef3f0cbd8df79d2143efd902;hpb=89e21dbecca75a5320f50ecb53a39699f8ace8f1;p=helm.git
diff --git a/helm/software/matita/nlibrary/topology/igft.ma b/helm/software/matita/nlibrary/topology/igft.ma
index 3c0ba7090..d6043fba2 100644
--- a/helm/software/matita/nlibrary/topology/igft.ma
+++ b/helm/software/matita/nlibrary/topology/igft.ma
@@ -153,7 +153,7 @@ is a peculiarity of Matita (for example in CIC as implemented by Coq they are th
same). The additional restriction of not allowing the elimination of a CProp
toward a Type makes the theory of Matita minimal in the following sense:
-
+
Theorems proved in CIC as implemented in Matita can be reused in a classical
and impredicative framework (i.e. forcing Matita to collapse the hierarchy of
@@ -1168,15 +1168,7 @@ We now proceed with the proof of the infinity rule.
D*)
-
-alias symbol "exists" (instance 1) = "exists".
-alias symbol "covers" = "new covers set".
-alias symbol "covers" = "new covers".
-alias symbol "covers" = "new covers set".
-alias symbol "covers" = "new covers".
-alias symbol "covers" = "new covers set".
-alias symbol "covers" = "new covers".
-alias symbol "covers" = "new covers set".
+alias symbol "covers" (instance 3) = "new covers set".
ntheorem new_coverage_infinity:
âA:nAx.âU:Ω^A.âa:A. (âi:ð a. ðð¦[ð a i] â U) â a â U.
#A; #U; #a; (** screenshot "n-cov-inf-1". *)