From 5f45af1ac24064c065b85465a42a8d5f39b1b1a2 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 14 Nov 2019 14:45:15 +0100
Subject: [PATCH] Add lemma `later_exist_except_0`.

---
 theories/bi/derived_laws_sbi.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/theories/bi/derived_laws_sbi.v b/theories/bi/derived_laws_sbi.v
index fe60dc3a7..9953ed04b 100644
--- a/theories/bi/derived_laws_sbi.v
+++ b/theories/bi/derived_laws_sbi.v
@@ -187,6 +187,8 @@ Proof.
 Qed.
 Lemma later_exist_2 {A} (Φ : A → PROP) : (∃ a, ▷ Φ a) ⊢ ▷ (∃ a, Φ a).
 Proof. apply exist_elim; eauto using exist_intro. Qed.
+Lemma later_exist_except_0 {A} (Φ : A → PROP) : ▷ (∃ a, Φ a) ⊢ ◇ (∃ a, ▷ Φ a).
+Proof. apply later_exist_false. Qed.
 Lemma later_exist `{Inhabited A} (Φ : A → PROP) : ▷ (∃ a, Φ a) ⊣⊢ (∃ a, ▷ Φ a).
 Proof.
   apply: anti_symm; [|apply later_exist_2].
-- 
GitLab