From c6bcaadec94b75f99bac4895a2386fe3adc90eae Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 11 May 2020 20:02:56 +0200
Subject: [PATCH] Add lemma `exist_wand_forall`, similar to
 `exist_impl_forall`.

---
 theories/bi/derived_laws_bi.v | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/theories/bi/derived_laws_bi.v b/theories/bi/derived_laws_bi.v
index 724ffb34a..1127e290b 100644
--- a/theories/bi/derived_laws_bi.v
+++ b/theories/bi/derived_laws_bi.v
@@ -427,6 +427,15 @@ Proof. by apply forall_intro=> a; rewrite forall_elim. Qed.
 Lemma sep_forall_r {A} (Φ : A → PROP) Q : (∀ a, Φ a) ∗ Q ⊢ ∀ a, Φ a ∗ Q.
 Proof. by apply forall_intro=> a; rewrite forall_elim. Qed.
 
+Lemma exist_wand_forall {A} P (Ψ : A → PROP) :
+  ((∃ x : A, Ψ x) -∗ P) ⊣⊢ ∀ x : A, Ψ x -∗ P.
+Proof.
+  apply equiv_spec; split.
+  - apply forall_intro=>x. by rewrite -exist_intro.
+  - apply wand_intro_r, wand_elim_r', exist_elim=>x.
+    apply wand_intro_r. by rewrite (forall_elim x) wand_elim_r.
+Qed.
+
 Global Instance wand_iff_ne : NonExpansive2 (@bi_wand_iff PROP).
 Proof. solve_proper. Qed.
 Global Instance wand_iff_proper :
-- 
GitLab