A few integrations (closed an axiom in finset).

[helm.git] / matita / matita / lib / basics / logic.ma

diff --git a/matita/matita/lib/basics/logic.ma b/matita/matita/lib/basics/logic.ma
index b6a5d59b7e09a575ab43c3361cc33a0ae28eafdf..4b90f75181300bdaced20673e08e5d6420f4fbc1 100644 (file)
--- a/matita/matita/lib/basics/logic.ma
+++ b/matita/matita/lib/basics/logic.ma
@@ -91,21 +91,17 @@ unification hint 0 ≔ T,a,b;
 inductive True: Prop ≝  
 I : True.
 
-interpretation "logical true" 'true = True.
-
 inductive False: Prop ≝ .
 
-interpretation "logical false" 'false = False.
-
 (* ndefinition Not: Prop → Prop ≝
-λA. A → ⊥. *)
+λA. A → False. *)
 
 inductive Not (A:Prop): Prop ≝
-nmk: (A → ⊥) → Not A.
+nmk: (A → False) → Not A.
 
 interpretation "logical not" 'not x = (Not x).
 
-theorem absurd : ∀A:Prop. A → ¬A → ⊥.
+theorem absurd : ∀A:Prop. A → ¬A → False.
 #A #H #Hn (elim Hn); /2/; qed.
 
 (*
@@ -151,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 :=