snapshot for CSC

[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 1fb59f067aa3ab33ee8426597ce2f0e2f50ebc3c..6628e36ef5db5b481f46791215972857bfbc44b1 100644 (file)
--- 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).