some fixes

[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 feccae4786bb3ecc5e7ced048b79262209bdda82..8bba1228176ee0eea57c91bb723636f196916928 100644 (file)
--- a/helm/software/matita/nlibrary/topology/igft.ma
+++ b/helm/software/matita/nlibrary/topology/igft.ma
@@ -929,6 +929,7 @@ 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".
 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". *)  
@@ -1130,7 +1131,8 @@ nelim o;
 ##| #p; #IH; napply (subseteq_intersection_r … IH);
     #x; #Hx; #i; ncases (H … Hx i); #c; *; *; #d; #Ed; #cG;
     @d; napply IH;
-    napply (. Ed^-1‡#); napply cG;    
+    alias symbol "prop2" = "prop21".
+napply (. Ed^-1‡#); napply cG;    
 ##| #a; #i; #f; #Hf; nchange with (G ⊆ { y | ∀x. y ∈ F⎽(f x) }); 
     #b; #Hb; #d; napply (Hf d); napply Hb;
 ##]