update in binaries for λδ

[helm.git] / helm / software / matita / nlibrary / topology / igft.ma

diff --git a/helm/software/matita/nlibrary/topology/igft.ma b/helm/software/matita/nlibrary/topology/igft.ma
index 3c0ba7090406c43aef3f0cbd8df79d2143efd902..d6043fba2c1d413fc22626fd567e18dbc34c5779 100644 (file)
--- 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: 
 
-<object class="img" data="igft-minimality-CIC.svg" type="image/svg+xml" width="500px"/>
+<object class="img" data="igft-minimality-CIC.svg" type="image/svg+xml" width="600px"/>
 
 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". *)