X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda%2Fpreamble.ma;h=c272595a2831f306ed7c12961cda21e2fa35bbf6;hb=30961a10d1cdfd74c4a662082419b717b85d63a6;hp=8e4b8fc962c0859991ec63c5c9c41e71d3e28ff9;hpb=6b87a3e9d6dd7c3abb922750587444ac3fd08e16;p=helm.git

diff --git a/matita/matita/contribs/lambda/preamble.ma b/matita/matita/contribs/lambda/preamble.ma
index 8e4b8fc96..c272595a2 100644
--- a/matita/matita/contribs/lambda/preamble.ma
+++ b/matita/matita/contribs/lambda/preamble.ma
@@ -28,10 +28,6 @@ notation "⊥"
   non associative with precedence 90
   for @{'false}.
 
-lemma ex2_1_commute: ∀A0. ∀P0,P1:A0→Prop. (∃∃x0. P0 x0 & P1 x0) → ∃∃x0. P1 x0 & P0 x0.
-#A0 #P0 #P1 * /2 width=3/
-qed.
-
 (* relations *)
 
 definition confluent1: ∀A. relation A → predicate A ≝ λA,R,a0.
@@ -42,6 +38,11 @@ definition confluent1: ∀A. relation A → predicate A ≝ λA,R,a0.
 definition confluent: ∀A. predicate (relation A) ≝ λA,R.
                       ∀a0. confluent1 … R a0.
 
+(* booleans *)
+
+definition is_false: predicate bool ≝ λb.
+                     false = b.
+
 (* arithmetics *)
 
 lemma lt_refl_false: ∀n. n < n → ⊥.