X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Flogic%2Fconnectives.ma;h=4d085995d4ea1a589af54e8552afdbe2fbf713e3;hb=2b98af47f4359ca20b42e52285c7ff4a3bd12f02;hp=34661dc8015e62a19403fb16e337359acb59c19e;hpb=8b1a49bbee9eea86eb74c040defe701370ca5893;p=helm.git

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