refactoring completed!

[helm.git] / matita / matita / lib / basics / bool.ma

diff --git a/matita/matita/lib/basics/bool.ma b/matita/matita/lib/basics/bool.ma
index adbfd9cab304d0455ac9626ed3203602384b2734..ce857937c6b5e766e9939a3a16008e373ea8d050 100644 (file)
--- 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 ].