From 25387faa6a72e489b68e9c092c3b2c79a77e7dcf Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 16 Feb 2017 16:42:40 +0100
Subject: [PATCH] =?UTF-8?q?Rename=20set=5FForall=5Fweaken=20=E2=86=92=20se?=
 =?UTF-8?q?t=5FForall=5Fimpl.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

To make it consistent with Forall_impl and map_Forall_impl. Also, put
the premises in the same order as those lemmas.
---
 theories/collections.v | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/theories/collections.v b/theories/collections.v
index 5d560497..a37e1365 100644
--- a/theories/collections.v
+++ b/theories/collections.v
@@ -820,11 +820,11 @@ End quantifiers.
 Section more_quantifiers.
   Context `{SimpleCollection A B}.
 
-  Lemma set_Forall_weaken (P Q : A → Prop) (Hweaken : ∀ x, P x → Q x) X :
-    set_Forall P X → set_Forall Q X.
+  Lemma set_Forall_impl (P Q : A → Prop) X :
+    set_Forall P X → (∀ x, P x → Q x) → set_Forall Q X.
   Proof. unfold set_Forall. naive_solver. Qed.
-  Lemma set_Exists_weaken (P Q : A → Prop) (Hweaken : ∀ x, P x → Q x) X :
-    set_Exists P X → set_Exists Q X.
+  Lemma set_Exists_impl (P Q : A → Prop) X :
+    set_Exists P X → (∀ x, P x → Q x) → set_Exists Q X.
   Proof. unfold set_Exists. naive_solver. Qed.
 End more_quantifiers.
 
-- 
GitLab