- new notation.ma file with local and common notation

[helm.git] / helm / software / matita / contribs / formal_topology / overlap / cprop_connectives.ma

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 644acc2183a3d813951252fd8921a175f4b5c340..59473882d6663d8b92ce8de55d31b63124fb7da2 100644 (file)
--- 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).