From d3a4d722fe4ba2849fa3661fc30365fb3a8777ad Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 25 Mar 2020 15:24:21 +0100
Subject: [PATCH] =?UTF-8?q?Prove=20`Laterable=20(=E2=88=83=20x,=20=CE=A6?=
 =?UTF-8?q?=20x)`.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/bi/lib/laterable.v | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/theories/bi/lib/laterable.v b/theories/bi/lib/laterable.v
index 764921828..648da0700 100644
--- a/theories/bi/lib/laterable.v
+++ b/theories/bi/lib/laterable.v
@@ -55,6 +55,14 @@ Section instances.
     - iApply "HQ". done.
   Qed.
 
+  Global Instance exist_laterable {A} (Φ : A → PROP) :
+    (∀ x, Laterable (Φ x)) → Laterable (∃ x, Φ x).
+  Proof.
+    rewrite /Laterable. iIntros (LΦ). iDestruct 1 as (x) "H".
+    iDestruct (LΦ with "H") as (Q) "[HQ #HΦ]".
+    iExists Q. iIntros "{$HQ} !# HQ". iExists x. by iApply "HΦ".
+  Qed.
+
   Global Instance big_sepL_laterable Ps :
     Timeless (PROP:=PROP) emp →
     TCForall Laterable Ps →
-- 
GitLab