X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fbasics%2Fbool.ma;h=ce857937c6b5e766e9939a3a16008e373ea8d050;hb=78f21d7d9014e5c7655f58239e4f1a128ea2c558;hp=adbfd9cab304d0455ac9626ed3203602384b2734;hpb=53452958508001e7af3090695b619fe92135fb9e;p=helm.git

diff --git a/matita/matita/lib/basics/bool.ma b/matita/matita/lib/basics/bool.ma
index adbfd9cab..ce857937c 100644
--- a/matita/matita/lib/basics/bool.ma
+++ b/matita/matita/lib/basics/bool.ma
@@ -16,10 +16,9 @@ inductive bool: Type[0] ≝
   | true : bool
   | false : bool.
 
-(* destruct does not work *)
 theorem not_eq_true_false : true ≠ false.
-@nmk #Heq change with match true with [true ⇒ False|false ⇒ True]
->Heq // qed.
+@nmk #Heq destruct
+qed.
 
 definition notb : bool → bool ≝
 λ b:bool. match b with [true ⇒ false|false ⇒ true ].