diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index ca50081f0b85b49f762cb880da322bb4ff12e0b8..d7d8a9a8c2e7928e1444994919448b51f8fb987f 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -138,7 +138,7 @@ Global Instance forall_flip_mono' A :
   Proper (pointwise_relation _ (flip (⊢)) ==> flip (⊢)) (@uPred_forall M A).
 Proof. intros P1 P2; apply forall_mono. Qed.
 Global Instance exist_mono' A :
-  Proper (pointwise_relation _ (flip (⊢)) ==> flip (⊢)) (@uPred_exist M A).
+  Proper (pointwise_relation _ (⊢) ==> (⊢)) (@uPred_exist M A).
 Proof. intros P1 P2; apply exist_mono. Qed.
 Global Instance exist_flip_mono' A :
   Proper (pointwise_relation _ (flip (⊢)) ==> flip (⊢)) (@uPred_exist M A).