some theorems have been moved to more appropriate files in library.

[helm.git] / matita / library / datatypes / bool.ma

diff --git a/matita/library/datatypes/bool.ma b/matita/library/datatypes/bool.ma
index b5abbb35d2b3748630fcc3faee802b9f608e7433..37a2a377d6fd39320fc8dfbdeeb1820de0fd1b25 100644 (file)
--- a/matita/library/datatypes/bool.ma
+++ b/matita/library/datatypes/bool.ma
@@ -163,11 +163,10 @@ elim A;
     reflexivity.
 qed.
 
-theorem andb_t_t_t: \forall A,B,C:bool.
-A = true \to B = true \to C = true \to (A \land (B \land C)) = true.
+theorem true_to_true_to_andb_true: \forall A,B:bool.
+A = true \to B = true \to (A \land B) = true.
 intros.
 rewrite > H.
 rewrite > H1.
-rewrite > H2.
 reflexivity.
 qed.
\ No newline at end of file