Merge branch 'robbert/later_exist_except_0' into 'master'

Add lemma `later_exist_except_0`. See merge request iris/iris!337

Merge branch 'robbert/later_exist_except_0' into 'master'
Add lemma `later_exist_except_0`. See merge request iris/iris!337
57dbcba0 · Ralf Jung · 263ab0d2 · 5f45af1a · 57dbcba0
Commit 57dbcba0 authored 5 years ago by Ralf Jung
--- 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].