Porting the new definition of equality.

diff --git a/helm/software/matita/nlibrary/basics/bool.ma b/helm/software/matita/nlibrary/basics/bool.ma
index b8153d701ffd3d634402b8a8b24c71ff2724469a..5b93813f0f8377a9c97cb97b48645b99370912f2 100644 (file)
--- 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.