From fcf38b87e9f21c84ce03be8305ad5f13a171ed3f Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 9 Feb 2016 12:45:39 +0100
Subject: [PATCH] fix and_exist_r

---
 program_logic/upred.v | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/program_logic/upred.v b/program_logic/upred.v
index 8bc3c0ec8..e07d358da 100644
--- a/program_logic/upred.v
+++ b/program_logic/upred.v
@@ -560,8 +560,11 @@ Proof.
   - apply exist_elim=>a. apply and_intro; first by rewrite and_elim_l.
     by rewrite -(exist_intro a) and_elim_r.
 Qed.
-Lemma and_exist_r {A} P (Q : A → uPred M) : (P ∧ ∃ a, Q a)%I ≡ (∃ a, P ∧ Q a)%I.
-Proof. by rewrite (commutative _ P) -and_exist_l (commutative _ P). Qed.
+Lemma and_exist_r {A} P (Q : A → uPred M) : ((∃ a, Q a) ∧ P)%I ≡ (∃ a, Q a ∧ P)%I.
+Proof.
+  rewrite -(commutative _ P) and_exist_l.
+  apply exist_proper=>a. by rewrite commutative.
+Qed.
 
 (* BI connectives *)
 Lemma sep_mono P P' Q Q' : P ⊑ Q → P' ⊑ Q' → (P ★ P') ⊑ (Q ★ Q').
-- 
GitLab