From e37edc7e31dffb47c312a9421172c19bbb2ec049 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 17 Jan 2018 00:39:29 +0100
Subject: [PATCH] Relate `forallb`/`existsb` to `Forall`/`Exists`.

---
 theories/list.v | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/theories/list.v b/theories/list.v
index b8a79c79..ace7fc83 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -2331,6 +2331,11 @@ Section Forall_Exists.
     end.
 End Forall_Exists.
 
+Lemma forallb_True (f : A → bool) xs : forallb f xs ↔ Forall f xs.
+Proof. split. induction xs; naive_solver. induction 1; naive_solver. Qed.
+Lemma existb_True (f : A → bool) xs : existsb f xs ↔ Exists f xs.
+Proof. split. induction xs; naive_solver. induction 1; naive_solver. Qed.
+
 Lemma replicate_as_Forall (x : A) n l :
   replicate n x = l ↔ length l = n ∧ Forall (x =) l.
 Proof. rewrite replicate_as_elem_of, Forall_forall. naive_solver. Qed.
-- 
GitLab