From cbf274c099afdc0cdf4f934bc554010209d77883 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 17 Nov 2016 23:29:18 +0100
Subject: [PATCH] Existentials commute with disjunction.

---
 base_logic/derived.v | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/base_logic/derived.v b/base_logic/derived.v
index 5d1483a7e..95150ab85 100644
--- a/base_logic/derived.v
+++ b/base_logic/derived.v
@@ -199,6 +199,13 @@ Lemma and_exist_r {A} P (Φ: A → uPred M) : (∃ a, Φ a) ∧ P ⊣⊢ ∃ a,
 Proof.
   rewrite -(comm _ P) and_exist_l. apply exist_proper=>a. by rewrite comm.
 Qed.
+Lemma or_exist {A} (Φ Ψ : A → uPred M) :
+  (∃ a, Φ a ∨ Ψ a) ⊣⊢ (∃ a, Φ a) ∨ (∃ a, Ψ a).
+Proof.
+  apply (anti_symm (⊢)).
+  - apply exist_elim=> a. by rewrite -!(exist_intro a).
+  - apply or_elim; apply exist_elim=> a; rewrite -(exist_intro a); auto.
+Qed.
 
 Lemma pure_mono φ1 φ2 : (φ1 → φ2) → ■ φ1 ⊢ ■ φ2.
 Proof. intros; apply pure_elim with φ1; eauto. Qed.
-- 
GitLab