From bac3136bf99a18374b91e1ec900e455567e8f741 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 6 Oct 2009 15:04:00 +0000
Subject: [PATCH] some fixes

---
 helm/software/matita/nlibrary/hints_declaration.ma |  4 ++--
 helm/software/matita/nlibrary/logic/connectives.ma |  5 +++++
 helm/software/matita/nlibrary/sets/sets.ma         | 12 ++++++++++++
 3 files changed, 19 insertions(+), 2 deletions(-)

diff --git a/helm/software/matita/nlibrary/hints_declaration.ma b/helm/software/matita/nlibrary/hints_declaration.ma
index dac148e4f..f91949be9 100644
--- a/helm/software/matita/nlibrary/hints_declaration.ma
+++ b/helm/software/matita/nlibrary/hints_declaration.ma
@@ -57,10 +57,10 @@ include "logic/pts.ma".
 
 ndefinition hint_declaration_Type0  ≝  λA:Type[0] .λa,b:A.Prop.
 ndefinition hint_declaration_Type1  ≝  λA:Type[1].λa,b:A.Prop.
-ndefinition hint_declaration_Type2  ≝  λa,b:Type[1].Prop.
+ndefinition hint_declaration_Type2  ≝  λa,b:Type[2].Prop.
 ndefinition hint_declaration_CProp0 ≝  λA:CProp[0].λa,b:A.Prop.
 ndefinition hint_declaration_CProp1 ≝  λA:CProp[1].λa,b:A.Prop.
-ndefinition hint_declaration_CProp2 ≝  λa,b:CProp[1].Prop.
+ndefinition hint_declaration_CProp2 ≝  λa,b:CProp[2].Prop.
   
 interpretation "hint_decl_Type2"  'hint_decl a b = (hint_declaration_Type2 a b).
 interpretation "hint_decl_CProp2" 'hint_decl a b = (hint_declaration_CProp2 a b).
diff --git a/helm/software/matita/nlibrary/logic/connectives.ma b/helm/software/matita/nlibrary/logic/connectives.ma
index 34661dc80..4d085995d 100644
--- a/helm/software/matita/nlibrary/logic/connectives.ma
+++ b/helm/software/matita/nlibrary/logic/connectives.ma
@@ -45,6 +45,11 @@ ninductive Ex1 (A:Type[1]) (P:A → CProp[0]) : CProp[1] ≝
 interpretation "exists1" 'exists x = (Ex1 ? x).
 interpretation "exists" 'exists x = (Ex ? x).
 
+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). 
+
 nrecord iff (A,B: CProp[0]) : CProp[0] ≝
  { if: A → B;
    fi: B → A
diff --git a/helm/software/matita/nlibrary/sets/sets.ma b/helm/software/matita/nlibrary/sets/sets.ma
index 3d03887ec..0e2dd418d 100644
--- a/helm/software/matita/nlibrary/sets/sets.ma
+++ b/helm/software/matita/nlibrary/sets/sets.ma
@@ -351,6 +351,18 @@ nrecord isomorphism (A, B : setoid) (S: ext_powerclass A) (T: ext_powerclass B)
    f_inj: injective … S iso_f
  }.
 
+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. 
+
 (*
 nrecord isomorphism (A, B : setoid) (S: qpowerclass A) (T: qpowerclass B) : CProp[0] ≝
  { iso_f:> unary_morphism A B;
-- 
2.39.2