From 9b27b913b9084226d0af5306562d0a1c5ccdaaf7 Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Thu, 18 Mar 2010 11:06:34 +0000
Subject: [PATCH] Porting the new definition of equality.

---
 helm/software/matita/nlibrary/basics/bool.ma | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

diff --git a/helm/software/matita/nlibrary/basics/bool.ma b/helm/software/matita/nlibrary/basics/bool.ma
index b8153d701..5b93813f0 100644
--- a/helm/software/matita/nlibrary/basics/bool.ma
+++ b/helm/software/matita/nlibrary/basics/bool.ma
@@ -33,7 +33,8 @@ qed.*)
 
 (* ndestrcut does not work *)
 ntheorem not_eq_true_false : true \neq false.
-#Heq; nchange with match true with [true ⇒ False|false ⇒ True];
+napply nmk; #Heq;
+nchange with match true with [true ⇒ False|false ⇒ True];
 nrewrite > Heq; //; nqed.
 
 ndefinition notb : bool → bool ≝
@@ -107,10 +108,15 @@ ndefinition if_then_else: ∀A:Type. bool → A → A → A ≝
  [ true ⇒ P
  | false  ⇒ Q].
 
+(*
+ntheorem fff: false ≠ true.
+/2/;
+//; nqed. *)
+
 ntheorem bool_to_decidable_eq:
  ∀b1,b2:bool. decidable (b1=b2).
 #b1; #b2; ncases b1; ncases b2; /2/;
-@2;/2/; nqed.
+@2;/3/; nqed.
 
 ntheorem true_or_false:
 ∀b:bool. b = true ∨ b = false.
-- 
2.39.2