diff --git a/theories/bi/lib/laterable.v b/theories/bi/lib/laterable.v
index 7649218284d74d91056f776da374fcc4ba82af8a..648da070094d980f4af3ade74125e58286d14526 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 →