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.