removed useless stuff

diff --git a/helm/software/matita/nlibrary/topology/igft.ma b/helm/software/matita/nlibrary/topology/igft.ma
index 8bba1228176ee0eea57c91bb723636f196916928..59ccd56019a34b690063b71f830dfbed5729b4ea 100644 (file)
--- 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: