From 4cf7fb9874bcfb1c5b9c8af5f2288ba817f7e7ea Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Tue, 13 Sep 2016 11:18:08 +0200
Subject: [PATCH] Lemma [exists_impl_forall] for currying an exists into a
 forall.

---
 algebra/upred.v | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

diff --git a/algebra/upred.v b/algebra/upred.v
index 6ef8b4271..b4b5abe28 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -684,6 +684,15 @@ Proof.
   - by apply impl_intro_l; rewrite left_id.
 Qed.
 
+Lemma exists_impl_forall {A} P (Ψ : A → uPred M) :
+  ((∃ x : A, Ψ x) → P) ⊣⊢ ∀ x : A, Ψ x → P.
+Proof.
+  apply equiv_spec; split.
+  - apply forall_intro=>x. by rewrite -exist_intro.
+  - apply impl_intro_r, impl_elim_r', exist_elim=>x.
+    apply impl_intro_r. by rewrite (forall_elim x) impl_elim_r.
+Qed.
+
 Lemma or_and_l P Q R : P ∨ Q ∧ R ⊣⊢ (P ∨ Q) ∧ (P ∨ R).
 Proof.
   apply (anti_symm (⊢)); first auto.
@@ -817,7 +826,7 @@ Proof.
   intros P; unseal; split=> n x Hvalid; split.
   - intros (x1&x2&?&_&?); cofe_subst; eauto using uPred_mono, cmra_includedN_r.
   - by intros ?; exists (core x), x; rewrite cmra_core_l.
-Qed. 
+Qed.
 Global Instance sep_comm : Comm (⊣⊢) (@uPred_sep M).
 Proof.
   by intros P Q; unseal; split=> n x ?; split;
-- 
GitLab