Skip to content
Snippets Groups Projects
Commit 5f45af1a authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Add lemma `later_exist_except_0`.

parent 60647cc2
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/bi/derived_laws_sbi.v
+ 2
− 0
View file @ 5f45af1a
......@@ -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].
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment