diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index c5359862842f2ba3b766d572e1e9e617f63afc73..e6a124cacfd8f9a08bbc326fcc7eb639fad039c2 100644
--- a/theories/algebra/auth.v
+++ b/theories/algebra/auth.v
@@ -168,7 +168,7 @@ Section auth.
   Lemma auth_auth_frac_op_inv_L `{!LeibnizEquiv A} q a p b :
     ✓ (●{p} a ⋅ ●{q} b) → a = b.
   Proof. by apply view_auth_frac_op_inv_L. Qed.
-  Global Instance is_op_auth_auth_frac q q1 q2 a :
+  Global Instance auth_auth_frac_is_op q q1 q2 a :
     IsOp q q1 q2 → IsOp' (●{q} a) (●{q1} a) (●{q2} a).
   Proof. rewrite /auth_auth. apply _. Qed.
 
@@ -180,7 +180,7 @@ Section auth.
   Proof. apply view_frag_core. Qed.
   Global Instance auth_frag_core_id a : CoreId a → CoreId (◯ a).
   Proof. rewrite /auth_frag. apply _. Qed.
-  Global Instance is_op_auth_frag a b1 b2 :
+  Global Instance auth_frag_is_op a b1 b2 :
     IsOp a b1 b2 → IsOp' (◯ a) (◯ b1) (◯ b2).
   Proof. rewrite /auth_frag. apply _. Qed.
   Global Instance auth_frag_sep_homomorphism :
diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index abb9a6c8c3cd095b25ce12d44052a50fa28b92fd..99a95cb69b4b216fba64785c075386b3a02b489e 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -300,7 +300,7 @@ Proof. apply singleton_core. rewrite cmra_pcore_core //. Qed.
 Lemma singleton_op (i : K) (x y : A) :
   {[ i := x ]} â‹… {[ i := y ]} =@{gmap K A} {[ i := x â‹… y ]}.
 Proof. by apply (merge_singleton _ _ _ x y). Qed.
-Global Instance is_op_singleton i a a1 a2 :
+Global Instance singleton_is_op i a a1 a2 :
   IsOp a a1 a2 → IsOp' ({[ i := a ]} : gmap K A) {[ i := a1 ]} {[ i := a2 ]}.
 Proof. rewrite /IsOp' /IsOp=> ->. by rewrite -singleton_op. Qed.
 
diff --git a/theories/algebra/lib/frac_auth.v b/theories/algebra/lib/frac_auth.v
index 5c4915c425a1f56dd5e1180a423f3ff2a9ef88ac..d317c918f4f84cc18754e89460a1aa2d44e28930 100644
--- a/theories/algebra/lib/frac_auth.v
+++ b/theories/algebra/lib/frac_auth.v
@@ -96,11 +96,11 @@ Section frac_auth.
   Lemma frac_auth_frag_valid_op_1_l q a b : ✓ (◯F{1} a ⋅ ◯F{q} b) → False.
   Proof. rewrite -frac_auth_frag_op frac_auth_frag_valid=> -[/exclusive_l []]. Qed.
 
-  Global Instance is_op_frac_auth (q q1 q2 : frac) (a a1 a2 : A) :
+  Global Instance frac_auth_is_op (q q1 q2 : frac) (a a1 a2 : A) :
     IsOp q q1 q2 → IsOp a a1 a2 → IsOp' (◯F{q} a) (◯F{q1} a1) (◯F{q2} a2).
   Proof. by rewrite /IsOp' /IsOp=> /leibniz_equiv_iff -> ->. Qed.
 
-  Global Instance is_op_frac_auth_core_id (q q1 q2 : frac) (a  : A) :
+  Global Instance frac_auth_is_op_core_id (q q1 q2 : frac) (a  : A) :
     CoreId a → IsOp q q1 q2 → IsOp' (◯F{q} a) (◯F{q1} a) (◯F{q2} a).
   Proof.
     rewrite /IsOp' /IsOp=> ? /leibniz_equiv_iff ->.
diff --git a/theories/algebra/lib/ufrac_auth.v b/theories/algebra/lib/ufrac_auth.v
index dab3a6d0a07ecc20dc5fd7d985a033bb44672c58..55261629d02e9a165335d527ab548ae8f48dc84a 100644
--- a/theories/algebra/lib/ufrac_auth.v
+++ b/theories/algebra/lib/ufrac_auth.v
@@ -111,11 +111,11 @@ Section ufrac_auth.
   Lemma ufrac_auth_frag_op q1 q2 a1 a2 : ◯U{q1+q2} (a1 ⋅ a2) ≡ ◯U{q1} a1 ⋅ ◯U{q2} a2.
   Proof. done. Qed.
 
-  Global Instance is_op_ufrac_auth q q1 q2 a a1 a2 :
+  Global Instance ufrac_auth_is_op q q1 q2 a a1 a2 :
     IsOp q q1 q2 → IsOp a a1 a2 → IsOp' (◯U{q} a) (◯U{q1} a1) (◯U{q2} a2).
   Proof. by rewrite /IsOp' /IsOp=> /leibniz_equiv_iff -> ->. Qed.
 
-  Global Instance is_op_ufrac_auth_core_id q q1 q2 a :
+  Global Instance ufrac_auth_is_op_core_id q q1 q2 a :
     CoreId a → IsOp q q1 q2 → IsOp' (◯U{q} a) (◯U{q1} a) (◯U{q2} a).
   Proof.
     rewrite /IsOp' /IsOp=> ? /leibniz_equiv_iff ->.
diff --git a/theories/algebra/namespace_map.v b/theories/algebra/namespace_map.v
index 7474b7e2c9c993969b46ae71e4ad353c13cc7112..ab55d9545b8570f2269dd1ea2b166d6de37239c8 100644
--- a/theories/algebra/namespace_map.v
+++ b/theories/algebra/namespace_map.v
@@ -218,7 +218,7 @@ Qed.
 Lemma namespace_map_data_mono N a b :
   a ≼ b → namespace_map_data N a ≼ namespace_map_data N b.
 Proof. intros [c ->]. rewrite namespace_map_data_op. apply cmra_included_l. Qed.
-Global Instance is_op_namespace_map_data N a b1 b2 :
+Global Instance namespace_map_data_is_op N a b1 b2 :
   IsOp a b1 b2 →
   IsOp' (namespace_map_data N a) (namespace_map_data N b1) (namespace_map_data N b2).
 Proof. rewrite /IsOp' /IsOp=> ->. by rewrite namespace_map_data_op. Qed.
diff --git a/theories/algebra/ufrac.v b/theories/algebra/ufrac.v
index 91fc0e8113786346786c8461fbcdf698410ce985..f6b3a44fc3a076fb4dcf1175d324a6214e7f777f 100644
--- a/theories/algebra/ufrac.v
+++ b/theories/algebra/ufrac.v
@@ -43,5 +43,5 @@ Qed.
 Lemma ufrac_op' (q p : ufrac) : (p â‹… q) = (p + q)%Qp.
 Proof. done. Qed.
 
-Global Instance is_op_ufrac (q : ufrac) : IsOp' q (q/2)%Qp (q/2)%Qp.
+Global Instance ufrac_is_op (q : ufrac) : IsOp' q (q/2)%Qp (q/2)%Qp.
 Proof. by rewrite /IsOp' /IsOp ufrac_op' Qp_div_2. Qed.
diff --git a/theories/algebra/view.v b/theories/algebra/view.v
index 94fe19030f2bdd6e054bad505417a068e2ce1be2..21541b73b361d30fe53b19a067a6ea8ed59f2585 100644
--- a/theories/algebra/view.v
+++ b/theories/algebra/view.v
@@ -318,7 +318,7 @@ Section cmra.
   Lemma view_auth_frac_op_inv_L `{!LeibnizEquiv A} p1 a1 p2 a2 :
     ✓ (●V{p1} a1 ⋅ ●V{p2} a2) → a1 = a2.
   Proof. by intros ?%view_auth_frac_op_inv%leibniz_equiv. Qed.
-  Global Instance is_op_view_auth_frac q q1 q2 a :
+  Global Instance view_auth_frac_is_op q q1 q2 a :
     IsOp q q1 q2 → IsOp' (●V{q} a) (●V{q1} a) (●V{q2} a).
   Proof. rewrite /IsOp' /IsOp => ->. by rewrite -view_auth_frac_op. Qed.
 
@@ -330,7 +330,7 @@ Section cmra.
   Proof. done. Qed.
   Global Instance view_frag_core_id b : CoreId b → CoreId (◯V b).
   Proof. do 2 constructor; simpl; auto. by apply core_id_core. Qed.
-  Global Instance is_op_view_frag b b1 b2 :
+  Global Instance view_frag_is_op b b1 b2 :
     IsOp b b1 b2 → IsOp' (◯V b) (◯V b1) (◯V b2).
   Proof. done. Qed.
   Global Instance view_frag_sep_homomorphism :