diff --git a/base_logic/primitive.v b/base_logic/primitive.v
index 299d9cd302d32367360ce69689d21d40e649e4cb..ed8841b31135c054c3ad34ee2462393a1196f3f2 100644
--- a/base_logic/primitive.v
+++ b/base_logic/primitive.v
@@ -322,6 +322,9 @@ Global Instance uPred_valid_proper : Proper ((⊣⊢) ==> iff) (@uPred_valid M).
 Proof. solve_proper. Qed.
 Global Instance uPred_valid_mono : Proper ((⊢) ==> impl) (@uPred_valid M).
 Proof. solve_proper. Qed.
+Global Instance uPred_valid_flip_mono :
+  Proper (flip (⊢) ==> flip impl) (@uPred_valid M).
+Proof. solve_proper. Qed.
 
 (** Introduction and elimination rules *)
 Lemma pure_intro φ P : φ → P ⊢ ⌜φ⌝.