From 1a11eaddca057bea4e1ea0b3c276fc5228e5b4b2 Mon Sep 17 00:00:00 2001
From: Olivier Laurent
Date: Mon, 4 May 2020 10:48:30 +0200
Subject: add incl_Forall_in_iff

---
 theories/Lists/List.v | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'theories')

diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index e4b87507f4..bdaaa91828 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -2968,6 +2968,10 @@ Section Exists_Forall.
     now apply neg_Forall_Exists_neg.
   Defined.
 
+  Lemma incl_Forall_in_iff l l' :
+    incl l l' <-> Forall (fun x => In x l') l.
+  Proof. now rewrite Forall_forall; split. Qed.
+
 End Exists_Forall.
 
 Hint Constructors Exists : core.
-- 
cgit v1.2.3