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=fb5c93c9812ea39fb78f1470da2095c80822e158;hp=d2acdb2bc79c4ad3e2862072d9567056407650d7;hpb=1e94683f160df35b31f1eee8f4d99a6ec8008b36;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..680cc4ac2 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/bool.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/bool.ma
@@ -32,6 +32,12 @@ 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