From 221946158c75dce388c1b7efe916674d26a87033 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 12 Sep 2005 11:27:47 +0000 Subject: [PATCH] Comment removed. --- helm/matita/library/nat/minimization.ma | 1 - 1 file changed, 1 deletion(-) diff --git a/helm/matita/library/nat/minimization.ma b/helm/matita/library/nat/minimization.ma index 8aa1deed3..da76606b4 100644 --- a/helm/matita/library/nat/minimization.ma +++ b/helm/matita/library/nat/minimization.ma @@ -44,7 +44,6 @@ definition max_spec \def \lambda f:nat \to bool.\lambda n: nat. ex nat (\lambda i:nat. (le i n) \land (f i = true)) \to (f n) = true \land (\forall i. i < n \to (f i = false)). -(* perche' si blocca per mezzo minuto qui ??? *) theorem f_max_true : \forall f:nat \to bool. \forall n:nat. ex nat (\lambda i:nat. (le i n) \land (f i = true)) \to f (max n f) = true. intros 2. -- 2.39.2