some fixes

diff --git a/helm/software/matita/nlibrary/hints_declaration.ma b/helm/software/matita/nlibrary/hints_declaration.ma
index dac148e4fe9f80f99fbd3fef5dc3e733c101d335..f91949be9f383f6b749be8388c414d795a3036a5 100644 (file)
--- 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 34661dc8015e62a19403fb16e337359acb59c19e..4d085995d4ea1a589af54e8552afdbe2fbf713e3 100644 (file)
--- 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 3d03887ec2e4a163292041486a977f596631b40c..0e2dd418d3c19ef4e00d02e02c8ed15c79175734 100644 (file)
--- 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;