diff --git a/program_logic/upred.v b/program_logic/upred.v
index 8bc3c0ec8b6fd28c1866503de38b85d5bc99111a..e07d358da5da9d36f3d29dd764e91c67a1f002a6 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').