X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Foverlap%2Fcprop_connectives.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Foverlap%2Fcprop_connectives.ma;h=59473882d6663d8b92ce8de55d31b63124fb7da2;hb=13114a0147a28f8c7359c9c19ee254716eb5f55a;hp=644acc2183a3d813951252fd8921a175f4b5c340;hpb=071d7a246190074c97e78192839e4bb5d5a1eef4;p=helm.git

diff --git a/helm/software/matita/contribs/formal_topology/overlap/cprop_connectives.ma b/helm/software/matita/contribs/formal_topology/overlap/cprop_connectives.ma
index 644acc218..59473882d 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/cprop_connectives.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/cprop_connectives.ma
@@ -142,6 +142,9 @@ interpretation "exT2 \snd" 'pi2b x y = (pi2exT23 _ _ _ _ x y).
 inductive exT2 (A:Type0) (P,Q:A→CProp0) : CProp0 ≝
   ex_introT2: ∀w:A. P w → Q w → exT2 A P Q.
 
+inductive exT22 (A:Type2) (P:A→CProp2) : CProp2 ≝
+  ex_introT22: ∀w:A. P w → exT22 A P.
+
 definition Not : CProp0 → Prop ≝ λx:CProp.x → False.
 
 interpretation "constructive not" 'not x = (Not x).