X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Fbasics%2Fbool.ma;h=5b93813f0f8377a9c97cb97b48645b99370912f2;hb=3e373f30525987b7b121ed74c8a1292dc71d185c;hp=b8153d701ffd3d634402b8a8b24c71ff2724469a;hpb=3ebf7fc2ebf1e7deb9cf860be3c5b540c8cf0b3e;p=helm.git

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.