diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index 464cb35e6d213729f2527caeffd0192d0ff04fac..ca50081f0b85b49f762cb880da322bb4ff12e0b8 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -236,6 +236,8 @@ Lemma pure_mono Ï†1 Ï†2 : (Ï†1 â†’ Ï†2) â†’ âŒœÏ†1âŒ âŠ¢ âŒœÏ†2âŒ.
 Proof. intros; apply pure_elim with Ï†1; eauto. Qed.
 Global Instance pure_mono' : Proper (impl ==> (âŠ¢)) (@uPred_pure M).
 Proof. intros Ï†1 Ï†2; apply pure_mono. Qed.
+Global Instance pure_flip_mono : Proper (flip impl ==> flip (âŠ¢)) (@uPred_pure M).
+Proof. intros Ï†1 Ï†2; apply pure_mono. Qed.
 Lemma pure_iff Ï†1 Ï†2 : (Ï†1 â†” Ï†2) â†’ âŒœÏ†1âŒ âŠ£âŠ¢ âŒœÏ†2âŒ.
 Proof. intros [??]; apply (anti_symm _); auto using pure_mono. Qed.
 Lemma pure_intro_l Ï† Q R : Ï† â†’ (âŒœÏ†âŒ âˆ§ Q âŠ¢ R) â†’ Q âŠ¢ R.