diff --git a/theories/bi/embedding.v b/theories/bi/embedding.v
index 4b7d4b2345f267a4cf0987ceb9c2b4774bcab1cb..635d39dc309c2e987f6cc96275efc176bd1a2245 100644
--- a/theories/bi/embedding.v
+++ b/theories/bi/embedding.v
@@ -42,7 +42,7 @@ Section bi_embedding.
 
   Global Instance bi_embed_proper : Proper ((≡) ==> (≡)) bi_embed.
   Proof. apply (ne_proper _). Qed.
-  Global Instance bi_embed_mono_flip : Proper (flip (⊢) ==> flip (⊢)) bi_embed.
+  Global Instance bi_embed_flip_mono : Proper (flip (⊢) ==> flip (⊢)) bi_embed.
   Proof. solve_proper. Qed.
   Global Instance bi_embed_inj : Inj (≡) (≡) bi_embed.
   Proof.
diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index 0ce6daec668ee7b9bc0d9fc1c120c1ba6315514f..511c267bfaaf3ede91e8db55c384da6efee4c1be 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -416,7 +416,7 @@ Implicit Types P Q : monPred.
 Global Instance monPred_at_mono :
   Proper ((⊢) ==> (⊑) ==> (⊢)) monPred_at.
 Proof. by move=> ?? [?] ?? ->. Qed.
-Global Instance monPred_at_mono_flip :
+Global Instance monPred_at_flip_mono :
   Proper (flip (⊢) ==> flip (⊑) ==> flip (⊢)) monPred_at.
 Proof. solve_proper. Qed.
 
@@ -426,7 +426,7 @@ Global Instance monPred_in_proper (R : relation I) :
 Proof. unseal. split. solve_proper. Qed.
 Global Instance monPred_in_mono : Proper (flip (⊑) ==> (⊢)) (@monPred_in I PROP).
 Proof. unseal. split. solve_proper. Qed.
-Global Instance monPred_in_mono_flip : Proper ((⊑) ==> flip (⊢)) (@monPred_in I PROP).
+Global Instance monPred_in_flip_mono : Proper ((⊑) ==> flip (⊢)) (@monPred_in I PROP).
 Proof. solve_proper. Qed.
 
 Global Instance monPred_positive : BiPositive PROP → BiPositive monPredI.