From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 6 Oct 2009 15:04:24 +0000 (+0000)
Subject: removed useless stuff
X-Git-Tag: make_still_working~3365
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3698de5ee6abc713534b0ee884e87e4046a087dd;p=helm.git

removed useless stuff
---

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: