X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Ftopology%2Figft.ma;h=59ccd56019a34b690063b71f830dfbed5729b4ea;hb=2f67829c12dea538114bb848e0275d220dba601b;hp=8bba1228176ee0eea57c91bb723636f196916928;hpb=1a4b02e346356b7e1be253f7660c1d617c1ffe0a;p=helm.git

diff --git a/helm/software/matita/nlibrary/topology/igft.ma b/helm/software/matita/nlibrary/topology/igft.ma
index 8bba12281..59ccd5601 100644
--- a/helm/software/matita/nlibrary/topology/igft.ma
+++ b/helm/software/matita/nlibrary/topology/igft.ma
@@ -116,26 +116,6 @@ D*)
 
 include "sets/sets.ma".
 
-(*HIDE*)
-(* move away *)
-nlemma subseteq_intersection_l: ∀A.∀U,V,W:Ω^A.U ⊆ W ∨ V ⊆ W → U ∩ V ⊆ W.
-#A; #U; #V; #W; *; #H; #x; *; #xU; #xV; napply H; nassumption;
-nqed.
-
-nlemma subseteq_union_l: ∀A.∀U,V,W:Ω^A.U ⊆ W → V ⊆ W → U ∪ V ⊆ W.
-#A; #U; #V; #W; #H; #H1; #x; *; #Hx; ##[ napply H; ##| napply H1; ##] nassumption;
-nqed. 
-
-nlemma subseteq_intersection_r: ∀A.∀U,V,W:Ω^A.W ⊆ U → W ⊆ V → W ⊆ U ∩ V.
-#A; #U; #V; #W; #H1; #H2; #x; #Hx; @; ##[ napply H1; ##| napply H2; ##] nassumption;
-nqed. 
-
-ninductive sigma (A : Type[0]) (P : A → CProp[0]) : Type[0] ≝ 
- sig_intro : ∀x:A.P x → sigma A P. 
-
-interpretation "sigma" 'sigma \eta.p = (sigma ? p). 
-(*UNHIDE*)
-
 (*D
 
 Some basic results that we will use are also part of the sets library: