X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Flib%2Fbool.ma;h=680cc4ac2afde0c61169bd9da1c0c78b7923bec5;hb=f16a572ff09aa3a0f9c8103914616ed49e7b4c29;hp=fed25ceda5ee8ce17d1c23c3e6e76e36401b5a8a;hpb=928cfe1ebf2fbd31731c8851cdec70802596016d;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 fed25ceda..680cc4ac2 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/bool.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/bool.ma
@@ -13,6 +13,7 @@
 (**************************************************************************)
 
 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".
 
@@ -22,9 +23,22 @@ interpretation "boolean false" 'no = false.
 
 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 eq_bool_dec: ∀b1,b2:bool. Decidable (b1 = b2).
+* * /2 width=1 by or_introl/
+@or_intror #H destruct
+qed-.