diff --git a/iris/algebra/agree.v b/iris/algebra/agree.v
index faf3437c2166fd464182b8de2f280da02c5e98bb..66bd3e41428ae432b82effa03540fe5f3c08ce81 100644
--- a/iris/algebra/agree.v
+++ b/iris/algebra/agree.v
@@ -94,7 +94,7 @@ Local Instance agree_pcore_instance : PCore (agree A) := Some.
 Lemma agree_validN_def n x :
   ✓{n} x ↔ ∀ a b, a ∈ agree_car x → b ∈ agree_car x → a ≡{n}≡ b.
 Proof.
-  rewrite /validN /agree_validN. destruct (agree_car _) as [|? [|??]]; auto.
+  rewrite /validN /agree_validN_instance. destruct (agree_car _) as [|? [|??]]; auto.
   setoid_rewrite elem_of_list_singleton; naive_solver.
 Qed.
 
@@ -194,7 +194,7 @@ Qed.
 
 Lemma to_agree_uninj x : ✓ x → ∃ a, to_agree a ≡ x.
 Proof.
-  rewrite /valid /agree_valid; setoid_rewrite agree_validN_def.
+  rewrite /valid /agree_valid_instance; setoid_rewrite agree_validN_def.
   destruct (elem_of_agree x) as [a ?].
   exists a; split=> b /=; setoid_rewrite elem_of_list_singleton; naive_solver.
 Qed.
diff --git a/iris/algebra/cmra.v b/iris/algebra/cmra.v
index 2f74c62b8071c6aa4baa59b07ad6e7f9850d0262..8c9ca92f21ee1ce65266763134da0603ea3c4bcb 100644
--- a/iris/algebra/cmra.v
+++ b/iris/algebra/cmra.v
@@ -1110,7 +1110,7 @@ Section prod.
   Local Instance prod_op_instance : Op (A * B) := λ x y, (x.1 ⋅ y.1, x.2 ⋅ y.2).
   Local Instance prod_pcore_instance : PCore (A * B) := λ x,
     c1 ← pcore (x.1); c2 ← pcore (x.2); Some (c1, c2).
-  Local Arguments prod_pcore !_ /.
+  Local Arguments prod_pcore_instance !_ /.
   Local Instance prod_valid_instance : Valid (A * B) := λ x, ✓ x.1 ∧ ✓ x.2.
   Local Instance prod_validN_instance : ValidN (A * B) := λ n x, ✓{n} x.1 ∧ ✓{n} x.2.
 
@@ -1121,7 +1121,7 @@ Section prod.
     pcore x ≡ Some cx ↔ pcore (x.1) ≡ Some (cx.1) ∧ pcore (x.2) ≡ Some (cx.2).
   Proof.
     split; [by intros (cx'&[-> ->]%prod_pcore_Some&->)%equiv_Some_inv_r'|].
-    rewrite {3}/pcore /prod_pcore. (* TODO: use setoid rewrite *)
+    rewrite {3}/pcore /prod_pcore_instance. (* TODO: use setoid rewrite *)
     intros [Hx1 Hx2]; inversion_clear Hx1; simpl; inversion_clear Hx2.
     by constructor.
   Qed.
@@ -1338,7 +1338,7 @@ Section option.
   Local Instance option_validN_instance : ValidN (option A) := λ n ma,
     match ma with Some a => ✓{n} a | None => True end.
   Local Instance option_pcore_instance : PCore (option A) := λ ma, Some (ma ≫= pcore).
-  Local Arguments option_pcore !_ /.
+  Local Arguments option_pcore_instance !_ /.
   Local Instance option_op_instance : Op (option A) := union_with (λ a b, Some (a ⋅ b)).
 
   Definition Some_valid a : ✓ Some a ↔ ✓ a := reflexivity _.
@@ -1399,9 +1399,9 @@ Section option.
     - eauto.
     - by intros [a|] n; destruct 1; constructor; ofe_subst.
     - destruct 1; by ofe_subst.
-    - by destruct 1; rewrite /validN /option_validN //=; ofe_subst.
+    - by destruct 1; rewrite /validN /option_validN_instance //=; ofe_subst.
     - intros [a|]; [apply cmra_valid_validN|done].
-    - intros n [a|]; unfold validN, option_validN; eauto using cmra_validN_S.
+    - intros n [a|]; unfold validN, option_validN_instance; eauto using cmra_validN_S.
     - intros [a|] [b|] [c|]; constructor; rewrite ?assoc; auto.
     - intros [a|] [b|]; constructor; rewrite 1?comm; auto.
     - intros [a|]; simpl; auto.
@@ -1414,7 +1414,7 @@ Section option.
         destruct (cmra_pcore_proper a b ca) as (?&?&?); eauto 10.
       + destruct (pcore a) as [ca|] eqn:?; eauto.
         destruct (cmra_pcore_mono a b ca) as (?&?&?); eauto 10.
-    - intros n [a|] [b|]; rewrite /validN /option_validN /=;
+    - intros n [a|] [b|]; rewrite /validN /option_validN_instance /=;
         eauto using cmra_validN_op_l.
     - intros n ma mb1 mb2.
       destruct ma as [a|], mb1 as [b1|], mb2 as [b2|]; intros Hx Hx';
@@ -1606,7 +1606,7 @@ Section discrete_fun_cmra.
   Definition discrete_fun_lookup_core f x : (core f) x = core (f x) := eq_refl.
 
   Lemma discrete_fun_included_spec_1 (f g : discrete_fun B) x : f ≼ g → f x ≼ g x.
-  Proof. by intros [h Hh]; exists (h x); rewrite /op /discrete_fun_op (Hh x). Qed.
+  Proof. by intros [h Hh]; exists (h x); rewrite /op /discrete_fun_op_instance (Hh x). Qed.
 
   Lemma discrete_fun_included_spec `{Hfin : Finite A} (f g : discrete_fun B) : f ≼ g ↔ ∀ x, f x ≼ g x.
   Proof.
diff --git a/iris/algebra/dfrac.v b/iris/algebra/dfrac.v
index b18d881119958f11d9460aaf7e7055b57f7212c3..e0329dbe3c7b8252770aaaf1caed39b58ad9358f 100644
--- a/iris/algebra/dfrac.v
+++ b/iris/algebra/dfrac.v
@@ -104,7 +104,7 @@ Section dfrac.
   Lemma dfrac_own_included q p : DfracOwn q ≼ DfracOwn p ↔ (q < p)%Qp.
   Proof.
     rewrite Qp_lt_sum. split.
-    - rewrite /included /op /dfrac_op. intros [[o| |?] [= ->]]. by exists o.
+    - rewrite /included /op /dfrac_op_instance. intros [[o| |?] [= ->]]. by exists o.
     - intros [o ->]. exists (DfracOwn o). by rewrite dfrac_op_own.
   Qed.
 
@@ -118,15 +118,15 @@ Section dfrac.
     split; try apply _.
     - intros [?| |?] ? dq <-; intros [= <-]; eexists _; done.
     - intros [?| |?] [?| |?] [?| |?];
-        rewrite /op /dfrac_op 1?assoc_L 1?assoc_L; done.
+        rewrite /op /dfrac_op_instance 1?assoc_L 1?assoc_L; done.
     - intros [?| |?] [?| |?];
-        rewrite /op /dfrac_op 1?(comm_L Qp_add); done.
-    - intros [?| |?] dq; rewrite /pcore /dfrac_pcore; intros [= <-];
-        rewrite /op /dfrac_op; done.
+        rewrite /op /dfrac_op_instance 1?(comm_L Qp_add); done.
+    - intros [?| |?] dq; rewrite /pcore /dfrac_pcore_instance; intros [= <-];
+        rewrite /op /dfrac_op_instance; done.
     - intros [?| |?] ? [= <-]; done.
     - intros [?| |?] [?| |?] ? [[?| |?] [=]] [= <-]; eexists _; split; try done;
         apply dfrac_discarded_included.
-    - intros [q| |q] [q'| |q']; rewrite /op /dfrac_op /valid /dfrac_valid //.
+    - intros [q| |q] [q'| |q']; rewrite /op /dfrac_op_instance /valid /dfrac_valid_instance //.
       + intros. trans (q + q')%Qp; [|done]. apply Qp_le_add_l.
       + apply Qp_lt_le_incl.
       + intros. trans (q + q')%Qp; [|by apply Qp_lt_le_incl]. apply Qp_le_add_l.
diff --git a/iris/algebra/list.v b/iris/algebra/list.v
index 6b4c8d6974ba8f44616f7fbc6c02716b77aebdf2..561a6fd0fe9bc30141c899634ab11f0d8dc79a69 100644
--- a/iris/algebra/list.v
+++ b/iris/algebra/list.v
@@ -195,13 +195,13 @@ Section cmra.
 
   Lemma list_lookup_valid l : ✓ l ↔ ∀ i, ✓ (l !! i).
   Proof.
-    rewrite {1}/valid /list_valid Forall_lookup; split.
+    rewrite {1}/valid /list_valid_instance Forall_lookup; split.
     - intros Hl i. by destruct (l !! i) as [x|] eqn:?; [apply (Hl i)|].
     - intros Hl i x Hi. move: (Hl i); by rewrite Hi.
   Qed.
   Lemma list_lookup_validN n l : ✓{n} l ↔ ∀ i, ✓{n} (l !! i).
   Proof.
-    rewrite {1}/validN /list_validN Forall_lookup; split.
+    rewrite {1}/validN /list_validN_instance Forall_lookup; split.
     - intros Hl i. by destruct (l !! i) as [x|] eqn:?; [apply (Hl i)|].
     - intros Hl i x Hi. move: (Hl i); by rewrite Hi.
   Qed.
diff --git a/iris/algebra/namespace_map.v b/iris/algebra/namespace_map.v
index 20674cd1603619495f8ab1829e6e441d1162b71d..ffe63bffae52b4046e6a9b9a28b83e5544e38674 100644
--- a/iris/algebra/namespace_map.v
+++ b/iris/algebra/namespace_map.v
@@ -99,7 +99,7 @@ Local Instance namespace_map_valid_instance : Valid (namespace_map A) := λ x,
      ∀ i, namespace_map_data_proj x !! i = None ∨ i ∉ E
   | CoPsetBot => False
   end.
-Global Arguments namespace_map_valid !_ /.
+Global Arguments namespace_map_valid_instance !_ /.
 Local Instance namespace_map_validN_instance : ValidN (namespace_map A) := λ n x,
   match namespace_map_token_proj x with
   | CoPset E =>
@@ -108,7 +108,7 @@ Local Instance namespace_map_validN_instance : ValidN (namespace_map A) := λ n
      ∀ i, namespace_map_data_proj x !! i = None ∨ i ∉ E
   | CoPsetBot => False
   end.
-Global Arguments namespace_map_validN !_ /.
+Global Arguments namespace_map_validN_instance !_ /.
 Local Instance namespace_map_pcore_instance : PCore (namespace_map A) := λ x,
   Some (NamespaceMap (core (namespace_map_data_proj x)) ε).
 Local Instance namespace_map_op_instance : Op (namespace_map A) := λ x y,
@@ -215,7 +215,7 @@ Proof. rewrite namespace_map_valid_eq /=. split; first done. by left. Qed.
 Lemma namespace_map_data_op N a b :
   namespace_map_data N (a â‹… b) = namespace_map_data N a â‹… namespace_map_data N b.
 Proof.
-  by rewrite {2}/op /namespace_map_op /namespace_map_data /= singleton_op left_id_L.
+  by rewrite {2}/op /namespace_map_op_instance /namespace_map_data /= singleton_op left_id_L.
 Qed.
 Lemma namespace_map_data_mono N a b :
   a ≼ b → namespace_map_data N a ≼ namespace_map_data N b.
@@ -229,7 +229,7 @@ Lemma namespace_map_token_union E1 E2 :
   E1 ## E2 →
   namespace_map_token (E1 ∪ E2) = namespace_map_token E1 ⋅ namespace_map_token E2.
 Proof.
-  intros. by rewrite /op /namespace_map_op
+  intros. by rewrite /op /namespace_map_op_instance
     /namespace_map_token /= coPset_disj_union // left_id_L.
 Qed.
 Lemma namespace_map_token_difference E1 E2 :
diff --git a/iris/algebra/numbers.v b/iris/algebra/numbers.v
index 5d778a4a2cd7772ae6c0114cbd1885ed9dc58401..c03951ac55f1a6da4a69aad38c6f6d2f9200e32e 100644
--- a/iris/algebra/numbers.v
+++ b/iris/algebra/numbers.v
@@ -62,7 +62,7 @@ Section max_nat.
   Proof.
     split.
     - intros [z ->]. simpl. lia.
-    - exists y. rewrite /op /max_nat_op. rewrite Nat.max_r; last lia. by destruct y.
+    - exists y. rewrite /op /max_nat_op_instance. rewrite Nat.max_r; last lia. by destruct y.
   Qed.
   Lemma max_nat_ra_mixin : RAMixin max_nat.
   Proof.
@@ -117,7 +117,7 @@ Section min_nat.
   Proof.
     split.
     - intros [z ->]. simpl. lia.
-    - exists y. rewrite /op /min_nat_op. rewrite Nat.min_r; last lia. by destruct y.
+    - exists y. rewrite /op /min_nat_op_instance. rewrite Nat.min_r; last lia. by destruct y.
   Qed.
   Lemma min_nat_ra_mixin : RAMixin min_nat.
   Proof.
diff --git a/iris/algebra/view.v b/iris/algebra/view.v
index 09f306b3a8c4b086a6eb0b090dd239a743cc7445..9989cafd4bf67e9651a866021084c42ce8a0464f 100644
--- a/iris/algebra/view.v
+++ b/iris/algebra/view.v
@@ -305,7 +305,7 @@ Section cmra.
   Lemma view_auth_frac_op_invN n p1 a1 p2 a2 :
     ✓{n} (●V{p1} a1 ⋅ ●V{p2} a2) → a1 ≡{n}≡ a2.
   Proof.
-    rewrite /op /view_op /= left_id -Some_op -pair_op view_validN_eq /=.
+    rewrite /op /view_op_instance /= left_id -Some_op -pair_op view_validN_eq /=.
     intros (?&?& Eq &?). apply (inj to_agree), agree_op_invN. by rewrite Eq.
   Qed.
   Lemma view_auth_frac_op_inv p1 a1 p2 a2 : ✓ (●V{p1} a1 ⋅ ●V{p2} a2) → a1 ≡ a2.