From 7626a698b525fa619aed3b60e1e039aa0048cf25 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 12 May 2017 11:31:27 +0200
Subject: [PATCH] =?UTF-8?q?Existentials=20distribute=20over=20=E2=97=87=20?=
 =?UTF-8?q?in=20both=20ways=20when=20the=20type=20is=20inhabited.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/base_logic/derived.v | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index 80faccdea..a7e08c030 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -692,8 +692,15 @@ Proof.
 Qed.
 Lemma except_0_forall {A} (Φ : A → uPred M) : ◇ (∀ a, Φ a) ⊢ ∀ a, ◇ Φ a.
 Proof. apply forall_intro=> a. by rewrite (forall_elim a). Qed.
-Lemma except_0_exist {A} (Φ : A → uPred M) : (∃ a, ◇ Φ a) ⊢ ◇ ∃ a, Φ a.
+Lemma except_0_exist_2 {A} (Φ : A → uPred M) : (∃ a, ◇ Φ a) ⊢ ◇ ∃ a, Φ a.
 Proof. apply exist_elim=> a. by rewrite (exist_intro a). Qed.
+Lemma except_0_exist `{Inhabited A} (Φ : A → uPred M) :
+  ◇ (∃ a, Φ a) ⊣⊢ (∃ a, ◇ Φ a).
+Proof.
+  apply (anti_symm _); [|by apply except_0_exist_2]. apply or_elim.
+  - rewrite -(exist_intro inhabitant). by apply or_intro_l.
+  - apply exist_mono=> a. apply except_0_intro.
+Qed.
 Lemma except_0_later P : ◇ ▷ P ⊢ ▷ P.
 Proof. by rewrite /uPred_except_0 -later_or False_or. Qed.
 Lemma except_0_always P : ◇ □ P ⊣⊢ □ ◇ P.
-- 
GitLab