X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Ftopology%2Figft.ma;h=6628e36ef5db5b481f46791215972857bfbc44b1;hb=f5f35ef830b1335dad2fcc3c1aae2b57815f73b1;hp=1fb59f067aa3ab33ee8426597ce2f0e2f50ebc3c;hpb=cb35a54563cbc0a531fc9c84d887b9e98f2d9378;p=helm.git

diff --git a/helm/software/matita/nlibrary/topology/igft.ma b/helm/software/matita/nlibrary/topology/igft.ma
index 1fb59f067..6628e36ef 100644
--- a/helm/software/matita/nlibrary/topology/igft.ma
+++ b/helm/software/matita/nlibrary/topology/igft.ma
@@ -74,6 +74,9 @@ nlet corec fish_rec (A:axiom_set) (U: Ω^A)
 nqed.
 
 (*
+alias symbol "covers" (instance 0) = "covers".
+alias symbol "covers" (instance 2) = "covers".
+alias symbol "covers" (instance 1) = "covers set".
 ntheorem covers_elim2:
  ∀A: axiom_set. ∀U:Ω^A.∀P: A → CProp[0].
   (∀a:A. a ∈ U → P a) →
@@ -101,6 +104,8 @@ nelim aU;
 ##]
 nqed.
 
+STOP
+
 definition leq ≝ λA:axiom_set.λa,b:A. a ◃ {y|b=y}.
 
 interpretation "covered by one" 'leq a b = (leq ? a b).