X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fbasics%2Flogic.ma;h=4b90f75181300bdaced20673e08e5d6420f4fbc1;hb=ea368a02a071bb99eeb84bf24ab4000acb314d60;hp=70e743e993ac96c12cdbf7a4a56cdc23bc8280b6;hpb=a87c9d012b588c381dc82c53fd0652762a9e50c9;p=helm.git

diff --git a/matita/matita/lib/basics/logic.ma b/matita/matita/lib/basics/logic.ma
index 70e743e99..4b90f7518 100644
--- a/matita/matita/lib/basics/logic.ma
+++ b/matita/matita/lib/basics/logic.ma
@@ -147,7 +147,13 @@ inductive ex (A:Type[0]) (P:A → Prop) : Prop ≝
 interpretation "exists" 'exists x = (ex ? x).
 
 inductive ex2 (A:Type[0]) (P,Q:A →Prop) : Prop ≝
-    ex_intro2: ∀ x:A. P x → Q x → ex2 A P Q.
+    ex2_intro: ∀ x:A. P x → Q x → ex2 A P Q.
+
+interpretation "exists on two predicates" 'exists2 x1 x2 = (ex2 ? x1 x2).
+
+lemma ex2_commute: ∀A0. ∀P0,P1:A0→Prop. (∃∃x0. P0 x0 & P1 x0) → ∃∃x0. P1 x0 & P0 x0.
+#A0 #P0 #P1 * /2 width=3/
+qed-.
 
 (* iff *)
 definition iff :=