X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Flib%2Fbool.ma;h=7dd817f979d62359d24432e908cd130f81529310;hb=1fd63df4c77f5c24024769432ea8492748b4ac79;hp=d2acdb2bc79c4ad3e2862072d9567056407650d7;hpb=67c5cf7ae14c745a94defbe645c5406ccbcf514d;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/bool.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/bool.ma
index d2acdb2bc..7dd817f97 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/bool.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/bool.ma
@@ -13,9 +13,9 @@
 (**************************************************************************)
 
 include "basics/bool.ma".
-include "ground_2/lib/star.ma".
-include "ground_2/notation/constructors/no_0.ma".
-include "ground_2/notation/constructors/yes_0.ma".
+include "ground_2/lib/relations.ma".
+include "ground_2/notation/functions/no_0.ma".
+include "ground_2/notation/functions/yes_0.ma".
 
 (* BOOLEAN PROPERTIES *******************************************************)
 
@@ -25,14 +25,35 @@ interpretation "boolean true" 'yes = true.
 
 (* Basic properties *********************************************************)
 
-lemma orb_false_r: ∀b1,b2:bool. (b1 ∨ b2) = false → b1 = false ∧ b2 = false.
-* normalize /2 width=1 by conj/ #b2 #H destruct
-qed-.
-
 lemma commutative_orb: commutative … orb.
 * * // qed.
 
+lemma orb_true_dx: ∀b. (b ∨ Ⓣ) = Ⓣ.
+* // qed.
+
+lemma orb_true_sn: ∀b. (Ⓣ ∨ b) = Ⓣ.
+// qed.
+
+lemma commutative_andb: commutative … andb.
+* * // qed.
+
+lemma andb_false_dx: ∀b. (b ∧ Ⓕ) = Ⓕ.
+* // qed.
+
+lemma andb_false_sn: ∀b. (Ⓕ ∧ b) = Ⓕ.
+// qed.
+
 lemma eq_bool_dec: ∀b1,b2:bool. Decidable (b1 = b2).
 * * /2 width=1 by or_introl/
 @or_intror #H destruct
 qed-.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma orb_inv_false_dx: ∀b1,b2:bool. (b1 ∨ b2) = Ⓕ → b1 = Ⓕ ∧ b2 = Ⓕ.
+* normalize /2 width=1 by conj/ #b2 #H destruct
+qed-.
+
+lemma andb_inv_true_dx: ∀b1,b2:bool. (b1 ∧ b2) = Ⓣ → b1 = Ⓣ ∧ b2 = Ⓣ.
+* normalize /2 width=1 by conj/ #b2 #H destruct
+qed-.