X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Flogic%2Fconnectives.ma;h=a149bc9ddf4e88133871e0d73aed62fe02fb613b;hb=12bebae6f57b3a671a1aa29662d5ed7208a85667;hp=25fb2ce93c38784c9069fe19dcf8e01551e5275a;hpb=5799dca87fe5c1b5a3cc1f4869109fe75d055ecd;p=helm.git

diff --git a/helm/software/matita/nlibrary/logic/connectives.ma b/helm/software/matita/nlibrary/logic/connectives.ma
index 25fb2ce93..a149bc9dd 100644
--- a/helm/software/matita/nlibrary/logic/connectives.ma
+++ b/helm/software/matita/nlibrary/logic/connectives.ma
@@ -38,4 +38,24 @@ interpretation "logical or" 'or x y = (Or x y).
 ninductive Ex (A:Type) (P:A → CProp) : CProp ≝
     ex_intro: ∀x:A. P x → Ex A P.
 
+
+ninductive Ex1 (A:Type[1]) (P:A → CProp) : CProp[1] ≝
+    ex_intro1: ∀x:A. P x → Ex1 A P.
+
+interpretation "exists1" 'exists x = (Ex1 ? x).
 interpretation "exists" 'exists x = (Ex ? x).
+
+nrecord iff (A,B: CProp) : CProp ≝
+ { if: A → B;
+   fi: B → A
+ }.
+
+notation > "hvbox(a break \liff b)"
+  left associative with precedence 25
+for @{ 'iff $a $b }.
+
+notation "hvbox(a break \leftrightarrow b)"
+  left associative with precedence 25
+for @{ 'iff $a $b }.
+
+interpretation "logical iff" 'iff x y = (iff x y).