diff --git a/theories/bi/derived_laws_sbi.v b/theories/bi/derived_laws_sbi.v
index fe60dc3a7f7ee6289979842b80f947504a754d8e..9953ed04bf3ed397da4b8ba4966295d2fc66b59e 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].