X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Ftopology%2Figft2.ma;h=90a644ce92c65b8e2ad81ec9ebcc66c130a253be;hb=6d0664747588f771e953c4d70f96e1cb5953d60e;hp=4703fba8c770659fc251fe5f0cf689e3a1f64653;hpb=7ae372991c6e02595c80bd4faaf437d39a965ce1;p=helm.git

diff --git a/helm/software/matita/nlibrary/topology/igft2.ma b/helm/software/matita/nlibrary/topology/igft2.ma
index 4703fba8c..90a644ce9 100644
--- a/helm/software/matita/nlibrary/topology/igft2.ma
+++ b/helm/software/matita/nlibrary/topology/igft2.ma
@@ -30,17 +30,11 @@ nlemma cover_ind':
             napply infty; nauto; ##] 
 nqed.
 
-alias symbol "covers" = "covers".
-alias symbol "covers" = "covers set".
-alias symbol "covers" = "covers".
-alias symbol "covers" = "covers set".
-alias symbol "covers" = "covers".
-alias symbol "covers" = "covers set".
+alias symbol "covers" (instance 1) = "covers".
 nlemma cover_ind'':
  ∀A:Ax.∀U:Ω^A.∀P:A → CProp[0].
   (∀a. a ∈ U → P a) → (∀a:A.∀j:𝐈 a. 𝐂 a j ◃ U → (∀b. b ∈ 𝐂 a j → P b) → P a) →
    ∀b. b ◃ U → P b.
-   
  #A; #U; #P; nletin V ≝ {x | P x}; napply (cover_ind' … V).
 nqed.
 
@@ -96,10 +90,8 @@ nrecord memdec (A: Type[0]) (U:Ω^A) : Type[0] ≝
 
 (*********** end from Cantor ********)
 
-alias symbol "covers" = "covers".
-alias symbol "covers" = "covers".
-alias symbol "covers" = "covers set".
-alias symbol "covers" = "covers set".
+alias symbol "covers" (instance 9) = "covers".
+alias symbol "covers" (instance 8) = "covers".
 nlet rec cover_rect
  (A:uuAx) (U:Ω^(uuax A)) (memdec: memdec … U) (P:uuax A → Type[0])
   (refl: ∀a:uuax A. a ∈ U → P a)