1) New file russell with the coercions to activate Russell-style proving.

[helm.git] / matita / matita / lib / basics / lists / listb.ma

diff --git a/matita/matita/lib/basics/lists/listb.ma b/matita/matita/lib/basics/lists/listb.ma
index f5bf4df9e43589533a511a307ff8281b3f10c1c0..29d89ffee85f5542e4e4ac20c46a073e73e33387 100644 (file)
--- a/matita/matita/lib/basics/lists/listb.ma
+++ b/matita/matita/lib/basics/lists/listb.ma
@@ -192,5 +192,16 @@ memb S x (filter ? f l) = true.
   ]
 qed. 
 
-
-
+(********************* exists *****************)
+
+let rec exists (A:Type[0]) (p:A → bool) (l:list A) on l : bool ≝
+match l with
+[ nil ⇒ false
+| cons h t ⇒ orb (p h) (exists A p t)
+].
+
+lemma Exists_exists : ∀A,P,l.
+  Exists A P l →
+  ∃x. P x.
+#A #P #l elim l [ * | #hd #tl #IH * [ #H %{hd} @H | @IH ]
+qed.