diff --git a/CHANGELOG.md b/CHANGELOG.md
index 824c082fcc92dd6d03525810792a2c02b59a9ba3..ed7c5c3bafcb1bc33715e36521649b1330c5b799 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -70,6 +70,9 @@ HeapLang, which is now in a separate package `coq-iris-heap-lang`.
   constructors `OfeT`→`Ofe`, `CmraT`→`Cmra`, and `UcmraT`→`Ucmra` since the `T`
   suffix is not needed. This change makes these names consistent with `bi`,
   which also does not have a `T` suffix.
+* Rename typeclass instances of CMRA operational typeclasses (`Op`, `Core`,
+  `PCore`, `Valid`, `ValidN`, `Unit`) to have a `_instance` suffix, so that
+  their original names are available to use as lemma names.
 
 **Changes in `bi`:**
 
diff --git a/iris/algebra/agree.v b/iris/algebra/agree.v
index 089456dee685d5e12f3b3ce3bbaf369b8c0b1490..66bd3e41428ae432b82effa03540fe5f3c08ce81 100644
--- a/iris/algebra/agree.v
+++ b/iris/algebra/agree.v
@@ -79,22 +79,22 @@ Canonical Structure agreeO := Ofe (agree A) agree_ofe_mixin.
 (* CMRA *)
 (* agree_validN is carefully written such that, when applied to a singleton, it
 is convertible to True. This makes working with agreement much more pleasant. *)
-Local Instance agree_validN : ValidN (agree A) := λ n x,
+Local Instance agree_validN_instance : ValidN (agree A) := λ n x,
   match agree_car x with
   | [a] => True
   | _ => ∀ a b, a ∈ agree_car x → b ∈ agree_car x → a ≡{n}≡ b
   end.
-Local Instance agree_valid : Valid (agree A) := λ x, ∀ n, ✓{n} x.
+Local Instance agree_valid_instance : Valid (agree A) := λ x, ∀ n, ✓{n} x.
 
-Program Instance agree_op : Op (agree A) := λ x y,
+Program Instance agree_op_instance : Op (agree A) := λ x y,
   {| agree_car := agree_car x ++ agree_car y |}.
 Next Obligation. by intros [[|??]] y. Qed.
-Local Instance agree_pcore : PCore (agree A) := Some.
+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 5ba38dff3b960267a4114a989cee78d81329be15..8c9ca92f21ee1ce65266763134da0603ea3c4bcb 100644
--- a/iris/algebra/cmra.v
+++ b/iris/algebra/cmra.v
@@ -1014,7 +1014,7 @@ Section discrete.
   Context (ra_mix : RAMixin A).
   Existing Instances discrete_dist.
 
-  Local Instance discrete_validN : ValidN A := λ n x, ✓ x.
+  Local Instance discrete_validN_instance : ValidN A := λ n x, ✓ x.
   Definition discrete_cmra_mixin : CmraMixin A.
   Proof.
     destruct ra_mix; split; try done.
@@ -1062,15 +1062,15 @@ End ra_total.
 
 (** ** CMRA for the unit type *)
 Section unit.
-  Local Instance unit_valid : Valid () := λ x, True.
-  Local Instance unit_validN : ValidN () := λ n x, True.
-  Local Instance unit_pcore : PCore () := λ x, Some x.
-  Local Instance unit_op : Op () := λ x y, ().
+  Local Instance unit_valid_instance : Valid () := λ x, True.
+  Local Instance unit_validN_instance : ValidN () := λ n x, True.
+  Local Instance unit_pcore_instance : PCore () := λ x, Some x.
+  Local Instance unit_op_instance : Op () := λ x y, ().
   Lemma unit_cmra_mixin : CmraMixin ().
   Proof. apply discrete_cmra_mixin, ra_total_mixin; by eauto. Qed.
   Canonical Structure unitR : cmra := Cmra unit unit_cmra_mixin.
 
-  Local Instance unit_unit : Unit () := ().
+  Local Instance unit_unit_instance : Unit () := ().
   Lemma unit_ucmra_mixin : UcmraMixin ().
   Proof. done. Qed.
   Canonical Structure unitUR : ucmra := Ucmra unit unit_ucmra_mixin.
@@ -1085,10 +1085,10 @@ End unit.
 
 (** ** CMRA for the empty type *)
 Section empty.
-  Local Instance Empty_set_valid : Valid Empty_set := λ x, False.
-  Local Instance Empty_set_validN : ValidN Empty_set := λ n x, False.
-  Local Instance Empty_set_pcore : PCore Empty_set := λ x, Some x.
-  Local Instance Empty_set_op : Op Empty_set := λ x y, x.
+  Local Instance Empty_set_valid_instance : Valid Empty_set := λ x, False.
+  Local Instance Empty_set_validN_instance : ValidN Empty_set := λ n x, False.
+  Local Instance Empty_set_pcore_instance : PCore Empty_set := λ x, Some x.
+  Local Instance Empty_set_op_instance : Op Empty_set := λ x y, x.
   Lemma Empty_set_cmra_mixin : CmraMixin Empty_set.
   Proof. apply discrete_cmra_mixin, ra_total_mixin; by (intros [] || done). Qed.
   Canonical Structure Empty_setR : cmra := Cmra Empty_set Empty_set_cmra_mixin.
@@ -1107,12 +1107,12 @@ Section prod.
   Local Arguments pcore _ _ !_ /.
   Local Arguments cmra_pcore _ !_/.
 
-  Local Instance prod_op : Op (A * B) := λ x y, (x.1 ⋅ y.1, x.2 ⋅ y.2).
-  Local Instance prod_pcore : PCore (A * B) := λ x,
+  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 Instance prod_valid : Valid (A * B) := λ x, ✓ x.1 ∧ ✓ x.2.
-  Local Instance prod_validN : ValidN (A * B) := λ n x, ✓{n} x.1 ∧ ✓{n} x.2.
+  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.
 
   Lemma prod_pcore_Some (x cx : A * B) :
     pcore x = Some cx ↔ pcore (x.1) = Some (cx.1) ∧ pcore (x.2) = Some (cx.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.
@@ -1230,7 +1230,7 @@ Global Arguments prodR : clear implicits.
 Section prod_unit.
   Context {A B : ucmra}.
 
-  Local Instance prod_unit `{Unit A, Unit B} : Unit (A * B) := (ε, ε).
+  Local Instance prod_unit_instance `{Unit A, Unit B} : Unit (A * B) := (ε, ε).
   Lemma prod_ucmra_mixin : UcmraMixin (A * B).
   Proof.
     split.
@@ -1333,13 +1333,13 @@ Section option.
   Local Arguments core _ _ !_ /.
   Local Arguments pcore _ _ !_ /.
 
-  Local Instance option_valid : Valid (option A) := λ ma,
+  Local Instance option_valid_instance : Valid (option A) := λ ma,
     match ma with Some a => ✓ a | None => True end.
-  Local Instance option_validN : ValidN (option A) := λ n ma,
+  Local Instance option_validN_instance : ValidN (option A) := λ n ma,
     match ma with Some a => ✓{n} a | None => True end.
-  Local Instance option_pcore : PCore (option A) := λ ma, Some (ma ≫= pcore).
-  Local Arguments option_pcore !_ /.
-  Local Instance option_op : Op (option A) := union_with (λ a b, Some (a ⋅ b)).
+  Local Instance option_pcore_instance : PCore (option A) := λ ma, Some (ma ≫= 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 _.
   Definition Some_validN a n : ✓{n} Some a ↔ ✓{n} 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';
@@ -1430,7 +1430,7 @@ Section option.
   Global Instance option_cmra_discrete : CmraDiscrete A → CmraDiscrete optionR.
   Proof. split; [apply _|]. by intros [a|]; [apply (cmra_discrete_valid a)|]. Qed.
 
-  Local Instance option_unit : Unit (option A) := None.
+  Local Instance option_unit_instance : Unit (option A) := None.
   Lemma option_ucmra_mixin : UcmraMixin optionR.
   Proof. split; [done|  |done]. by intros []. Qed.
   Canonical Structure optionUR := Ucmra (option A) option_ucmra_mixin.
@@ -1597,16 +1597,16 @@ Section discrete_fun_cmra.
   Context `{B : A → ucmra}.
   Implicit Types f g : discrete_fun B.
 
-  Local Instance discrete_fun_op : Op (discrete_fun B) := λ f g x, f x ⋅ g x.
-  Local Instance discrete_fun_pcore : PCore (discrete_fun B) := λ f, Some (λ x, core (f x)).
-  Local Instance discrete_fun_valid : Valid (discrete_fun B) := λ f, ∀ x, ✓ f x.
-  Local Instance discrete_fun_validN : ValidN (discrete_fun B) := λ n f, ∀ x, ✓{n} f x.
+  Local Instance discrete_fun_op_instance : Op (discrete_fun B) := λ f g x, f x ⋅ g x.
+  Local Instance discrete_fun_pcore_instance : PCore (discrete_fun B) := λ f, Some (λ x, core (f x)).
+  Local Instance discrete_fun_valid_instance : Valid (discrete_fun B) := λ f, ∀ x, ✓ f x.
+  Local Instance discrete_fun_validN_instance : ValidN (discrete_fun B) := λ n f, ∀ x, ✓{n} f x.
 
   Definition discrete_fun_lookup_op f g x : (f â‹… g) x = f x â‹… g x := eq_refl.
   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.
@@ -1642,7 +1642,7 @@ Section discrete_fun_cmra.
   Qed.
   Canonical Structure discrete_funR := Cmra (discrete_fun B) discrete_fun_cmra_mixin.
 
-  Local Instance discrete_fun_unit : Unit (discrete_fun B) := λ x, ε.
+  Local Instance discrete_fun_unit_instance : Unit (discrete_fun B) := λ x, ε.
   Definition discrete_fun_lookup_empty x : ε x = ε := eq_refl.
 
   Lemma discrete_fun_ucmra_mixin : UcmraMixin (discrete_fun B).
diff --git a/iris/algebra/coPset.v b/iris/algebra/coPset.v
index 0cd54e269c9c493753fc972c360beafcc7c2eb53..caa1be24dc28901a6c222f9daf4a2768230c3dc3 100644
--- a/iris/algebra/coPset.v
+++ b/iris/algebra/coPset.v
@@ -11,10 +11,10 @@ Section coPset.
 
   Canonical Structure coPsetO := discreteO coPset.
 
-  Local Instance coPset_valid : Valid coPset := λ _, True.
-  Local Instance coPset_unit : Unit coPset := (∅ : coPset).
-  Local Instance coPset_op : Op coPset := union.
-  Local Instance coPset_pcore : PCore coPset := Some.
+  Local Instance coPset_valid_instance : Valid coPset := λ _, True.
+  Local Instance coPset_unit_instance : Unit coPset := (∅ : coPset).
+  Local Instance coPset_op_instance : Op coPset := union.
+  Local Instance coPset_pcore_instance : PCore coPset := Some.
 
   Lemma coPset_op_union X Y : X ⋅ Y = X ∪ Y.
   Proof. done. Qed.
@@ -69,15 +69,15 @@ Section coPset_disj.
   Local Arguments op _ _ !_ !_ /.
   Canonical Structure coPset_disjO := leibnizO coPset_disj.
 
-  Local Instance coPset_disj_valid : Valid coPset_disj := λ X,
+  Local Instance coPset_disj_valid_instance : Valid coPset_disj := λ X,
     match X with CoPset _ => True | CoPsetBot => False end.
-  Local Instance coPset_disj_unit : Unit coPset_disj := CoPset ∅.
-  Local Instance coPset_disj_op : Op coPset_disj := λ X Y,
+  Local Instance coPset_disj_unit_instance : Unit coPset_disj := CoPset ∅.
+  Local Instance coPset_disj_op_instance : Op coPset_disj := λ X Y,
     match X, Y with
     | CoPset X, CoPset Y => if decide (X ## Y) then CoPset (X ∪ Y) else CoPsetBot
     | _, _ => CoPsetBot
     end.
-  Local Instance coPset_disj_pcore : PCore coPset_disj := λ _, Some ε.
+  Local Instance coPset_disj_pcore_instance : PCore coPset_disj := λ _, Some ε.
 
   Ltac coPset_disj_solve :=
     repeat (simpl || case_decide);
diff --git a/iris/algebra/csum.v b/iris/algebra/csum.v
index 72d750cb665121e3a4486599e0ed74ca5e3e1534..2d55fd1e3c6ca73752a8b25720262034bf2b6805 100644
--- a/iris/algebra/csum.v
+++ b/iris/algebra/csum.v
@@ -148,25 +148,25 @@ Implicit Types a : A.
 Implicit Types b : B.
 
 (* CMRA *)
-Local Instance csum_valid : Valid (csum A B) := λ x,
+Local Instance csum_valid_instance : Valid (csum A B) := λ x,
   match x with
   | Cinl a => ✓ a
   | Cinr b => ✓ b
   | CsumBot => False
   end.
-Local Instance csum_validN : ValidN (csum A B) := λ n x,
+Local Instance csum_validN_instance : ValidN (csum A B) := λ n x,
   match x with
   | Cinl a => ✓{n} a
   | Cinr b => ✓{n} b
   | CsumBot => False
   end.
-Local Instance csum_pcore : PCore (csum A B) := λ x,
+Local Instance csum_pcore_instance : PCore (csum A B) := λ x,
   match x with
   | Cinl a => Cinl <$> pcore a
   | Cinr b => Cinr <$> pcore b
   | CsumBot => Some CsumBot
   end.
-Local Instance csum_op : Op (csum A B) := λ x y,
+Local Instance csum_op_instance : Op (csum A B) := λ x y,
   match x, y with
   | Cinl a, Cinl a' => Cinl (a â‹… a')
   | Cinr b, Cinr b' => Cinr (b â‹… b')
diff --git a/iris/algebra/dfrac.v b/iris/algebra/dfrac.v
index ace017d6d2bef9d6c03b811f806d9cf77d7835ce..e0329dbe3c7b8252770aaaf1caed39b58ad9358f 100644
--- a/iris/algebra/dfrac.v
+++ b/iris/algebra/dfrac.v
@@ -62,7 +62,7 @@ Section dfrac.
   Proof. by injection 1. Qed.
 
   (** An element is valid as long as the sum of its content is less than one. *)
-  Local Instance dfrac_valid : Valid dfrac := λ dq,
+  Local Instance dfrac_valid_instance : Valid dfrac := λ dq,
     match dq with
     | DfracOwn q => q ≤ 1
     | DfracDiscarded => True
@@ -72,7 +72,7 @@ Section dfrac.
   (** As in the fractional camera the core is undefined for elements denoting
      ownership of a fraction. For elements denoting the knowledge that a fraction has
      been discarded the core is the identity function. *)
-  Local Instance dfrac_pcore : PCore dfrac := λ dq,
+  Local Instance dfrac_pcore_instance : PCore dfrac := λ dq,
     match dq with
     | DfracOwn q => None
     | DfracDiscarded => Some DfracDiscarded
@@ -81,7 +81,7 @@ Section dfrac.
 
   (** When elements are combined, ownership is added together and knowledge of
      discarded fractions is combined with the max operation. *)
-  Local Instance dfrac_op : Op dfrac := λ dq dp,
+  Local Instance dfrac_op_instance : Op dfrac := λ dq dp,
     match dq, dp with
     | DfracOwn q, DfracOwn q' => DfracOwn (q + q')
     | DfracOwn q, DfracDiscarded => DfracBoth q
@@ -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/dra.v b/iris/algebra/dra.v
index c3e7706afc90ac0846992badf15f23bceb6eef1f..b2b7ae2012c20ecb9796f8aa489baf75e6e4a260 100644
--- a/iris/algebra/dra.v
+++ b/iris/algebra/dra.v
@@ -107,7 +107,7 @@ Implicit Types a b : A.
 Implicit Types x y z : validity A.
 Local Arguments valid _ _ !_ /.
 
-Local Instance validity_valid : Valid (validity A) := validity_is_valid.
+Local Instance validity_valid_instance : Valid (validity A) := validity_is_valid.
 Local Instance validity_equiv : Equiv (validity A) := λ x y,
   (valid x ↔ valid y) ∧ (valid x → validity_car x ≡ validity_car y).
 Local Instance validity_equivalence : Equivalence (@equiv (validity A) _).
@@ -146,10 +146,10 @@ Local Hint Immediate dra_disjoint_move_l dra_disjoint_move_r : core.
 Lemma validity_valid_car_valid z : ✓ z → ✓ validity_car z.
 Proof. apply validity_prf. Qed.
 Local Hint Resolve validity_valid_car_valid : core.
-Program Instance validity_pcore : PCore (validity A) := λ x,
+Program Instance validity_pcore_instance : PCore (validity A) := λ x,
   Some (Validity (core (validity_car x)) (✓ x) _).
 Solve Obligations with naive_solver eauto using dra_core_valid.
-Program Instance validity_op : Op (validity A) := λ x y,
+Program Instance validity_op_instance : Op (validity A) := λ x y,
   Validity (validity_car x â‹… validity_car y)
            (✓ x ∧ ✓ y ∧ validity_car x ## validity_car y) _.
 Solve Obligations with naive_solver eauto using dra_op_valid.
diff --git a/iris/algebra/excl.v b/iris/algebra/excl.v
index 959fcf1ae1176adb75ddcf88e258cebc1d97242b..0dec359fbf0aa0cde084bcaa26672a78c4029676 100644
--- a/iris/algebra/excl.v
+++ b/iris/algebra/excl.v
@@ -70,12 +70,12 @@ Global Instance ExclBot_discrete : Discrete (@ExclBot A).
 Proof. by inversion_clear 1; constructor. Qed.
 
 (* CMRA *)
-Local Instance excl_valid : Valid (excl A) := λ x,
+Local Instance excl_valid_instance : Valid (excl A) := λ x,
   match x with Excl _ => True | ExclBot => False end.
-Local Instance excl_validN : ValidN (excl A) := λ n x,
+Local Instance excl_validN_instance : ValidN (excl A) := λ n x,
   match x with Excl _ => True | ExclBot => False end.
-Local Instance excl_pcore : PCore (excl A) := λ _, None.
-Local Instance excl_op : Op (excl A) := λ x y, ExclBot.
+Local Instance excl_pcore_instance : PCore (excl A) := λ _, None.
+Local Instance excl_op_instance : Op (excl A) := λ x y, ExclBot.
 
 Lemma excl_cmra_mixin : CmraMixin (excl A).
 Proof.
diff --git a/iris/algebra/frac.v b/iris/algebra/frac.v
index 9dd0a115661094c011376dfcc9b2649d8a8012f6..433b86a4ef76a36620b05972b9bdc923b8838b7a 100644
--- a/iris/algebra/frac.v
+++ b/iris/algebra/frac.v
@@ -15,9 +15,9 @@ Notation frac := Qp (only parsing).
 Section frac.
   Canonical Structure fracO := leibnizO frac.
 
-  Local Instance frac_valid : Valid frac := λ x, (x ≤ 1)%Qp.
-  Local Instance frac_pcore : PCore frac := λ _, None.
-  Local Instance frac_op : Op frac := λ x y, (x + y)%Qp.
+  Local Instance frac_valid_instance : Valid frac := λ x, (x ≤ 1)%Qp.
+  Local Instance frac_pcore_instance : PCore frac := λ _, None.
+  Local Instance frac_op_instance : Op frac := λ x y, (x + y)%Qp.
 
   Lemma frac_valid' p : ✓ p ↔ (p ≤ 1)%Qp.
   Proof. done. Qed.
diff --git a/iris/algebra/gmap.v b/iris/algebra/gmap.v
index 9774576484979d7fd064db2d00e83542cb6c05af..5dd69ba7813cbb1155d8b34acb09c6108807cf1a 100644
--- a/iris/algebra/gmap.v
+++ b/iris/algebra/gmap.v
@@ -141,11 +141,11 @@ Section cmra.
 Context `{Countable K} {A : cmra}.
 Implicit Types m : gmap K A.
 
-Local Instance gmap_unit : Unit (gmap K A) := (∅ : gmap K A).
-Local Instance gmap_op : Op (gmap K A) := merge op.
-Local Instance gmap_pcore : PCore (gmap K A) := λ m, Some (omap pcore m).
-Local Instance gmap_valid : Valid (gmap K A) := λ m, ∀ i, ✓ (m !! i).
-Local Instance gmap_validN : ValidN (gmap K A) := λ n m, ∀ i, ✓{n} (m !! i).
+Local Instance gmap_unit_instance : Unit (gmap K A) := (∅ : gmap K A).
+Local Instance gmap_op_instance : Op (gmap K A) := merge op.
+Local Instance gmap_pcore_instance : PCore (gmap K A) := λ m, Some (omap pcore m).
+Local Instance gmap_valid_instance : Valid (gmap K A) := λ m, ∀ i, ✓ (m !! i).
+Local Instance gmap_validN_instance : ValidN (gmap K A) := λ n m, ∀ i, ✓{n} (m !! i).
 
 Lemma lookup_op m1 m2 i : (m1 â‹… m2) !! i = m1 !! i â‹… m2 !! i.
 Proof. by apply lookup_merge. Qed.
diff --git a/iris/algebra/gmultiset.v b/iris/algebra/gmultiset.v
index 4f04081a113de953f73b6b7eabf3def88af590de..55523f169d0c6462e1b2c586f5f827af1fb9054c 100644
--- a/iris/algebra/gmultiset.v
+++ b/iris/algebra/gmultiset.v
@@ -10,11 +10,11 @@ Section gmultiset.
 
   Canonical Structure gmultisetO := discreteO (gmultiset K).
 
-  Local Instance gmultiset_valid : Valid (gmultiset K) := λ _, True.
-  Local Instance gmultiset_validN : ValidN (gmultiset K) := λ _ _, True.
-  Local Instance gmultiset_unit : Unit (gmultiset K) := (∅ : gmultiset K).
-  Local Instance gmultiset_op : Op (gmultiset K) := disj_union.
-  Local Instance gmultiset_pcore : PCore (gmultiset K) := λ X, Some ∅.
+  Local Instance gmultiset_valid_instance : Valid (gmultiset K) := λ _, True.
+  Local Instance gmultiset_validN_instance : ValidN (gmultiset K) := λ _ _, True.
+  Local Instance gmultiset_unit_instance : Unit (gmultiset K) := (∅ : gmultiset K).
+  Local Instance gmultiset_op_instance : Op (gmultiset K) := disj_union.
+  Local Instance gmultiset_pcore_instance : PCore (gmultiset K) := λ X, Some ∅.
 
   Lemma gmultiset_op_disj_union X Y : X ⋅ Y = X ⊎ Y.
   Proof. done. Qed.
diff --git a/iris/algebra/gset.v b/iris/algebra/gset.v
index 4f6ea4efe7dc2367a108ae9f098eafa16803f78f..1e740708f4ca1ef745d7721d513bdfdcfe042b25 100644
--- a/iris/algebra/gset.v
+++ b/iris/algebra/gset.v
@@ -10,10 +10,10 @@ Section gset.
 
   Canonical Structure gsetO := discreteO (gset K).
 
-  Local Instance gset_valid : Valid (gset K) := λ _, True.
-  Local Instance gset_unit : Unit (gset K) := (∅ : gset K).
-  Local Instance gset_op : Op (gset K) := union.
-  Local Instance gset_pcore : PCore (gset K) := λ X, Some X.
+  Local Instance gset_valid_instance : Valid (gset K) := λ _, True.
+  Local Instance gset_unit_instance : Unit (gset K) := (∅ : gset K).
+  Local Instance gset_op_instance : Op (gset K) := union.
+  Local Instance gset_pcore_instance : PCore (gset K) := λ X, Some X.
 
   Lemma gset_op_union X Y : X ⋅ Y = X ∪ Y.
   Proof. done. Qed.
@@ -85,15 +85,15 @@ Section gset_disj.
 
   Canonical Structure gset_disjO := leibnizO (gset_disj K).
 
-  Local Instance gset_disj_valid : Valid (gset_disj K) := λ X,
+  Local Instance gset_disj_valid_instance : Valid (gset_disj K) := λ X,
     match X with GSet _ => True | GSetBot => False end.
-  Local Instance gset_disj_unit : Unit (gset_disj K) := GSet ∅.
-  Local Instance gset_disj_op : Op (gset_disj K) := λ X Y,
+  Local Instance gset_disj_unit_instance : Unit (gset_disj K) := GSet ∅.
+  Local Instance gset_disj_op_instance : Op (gset_disj K) := λ X Y,
     match X, Y with
     | GSet X, GSet Y => if decide (X ## Y) then GSet (X ∪ Y) else GSetBot
     | _, _ => GSetBot
     end.
-  Local Instance gset_disj_pcore : PCore (gset_disj K) := λ _, Some ε.
+  Local Instance gset_disj_pcore_instance : PCore (gset_disj K) := λ _, Some ε.
 
   Ltac gset_disj_solve :=
     repeat (simpl || case_decide);
diff --git a/iris/algebra/list.v b/iris/algebra/list.v
index 5e7aea7323456360f40001eacdd6b7ce7b270a02..561a6fd0fe9bc30141c899634ab11f0d8dc79a69 100644
--- a/iris/algebra/list.v
+++ b/iris/algebra/list.v
@@ -172,17 +172,17 @@ Section cmra.
   Implicit Types l : list A.
   Local Arguments op _ _ !_ !_ / : simpl nomatch.
 
-  Local Instance list_op : Op (list A) :=
+  Local Instance list_op_instance : Op (list A) :=
     fix go l1 l2 := let _ : Op _ := @go in
     match l1, l2 with
     | [], _ => l2
     | _, [] => l1
     | x :: l1, y :: l2 => x â‹… y :: l1 â‹… l2
     end.
-  Local Instance list_pcore : PCore (list A) := λ l, Some (core <$> l).
+  Local Instance list_pcore_instance : PCore (list A) := λ l, Some (core <$> l).
 
-  Local Instance list_valid : Valid (list A) := Forall (λ x, ✓ x).
-  Local Instance list_validN : ValidN (list A) := λ n, Forall (λ x, ✓{n} x).
+  Local Instance list_valid_instance : Valid (list A) := Forall (λ x, ✓ x).
+  Local Instance list_validN_instance : ValidN (list A) := λ n, Forall (λ x, ✓{n} x).
 
   Lemma cons_valid l x : ✓ (x :: l) ↔ ✓ x ∧ ✓ l.
   Proof. apply Forall_cons. Qed.
@@ -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.
@@ -267,7 +267,7 @@ Section cmra.
   Qed.
   Canonical Structure listR := Cmra (list A) list_cmra_mixin.
 
-  Global Instance list_unit : Unit (list A) := [].
+  Global Instance list_unit_instance : Unit (list A) := [].
   Definition list_ucmra_mixin : UcmraMixin (list A).
   Proof.
     split.
diff --git a/iris/algebra/namespace_map.v b/iris/algebra/namespace_map.v
index eb2ee07d9e5e2093ce16a3709c4ad64f2c03f4a9..ffe63bffae52b4046e6a9b9a28b83e5544e38674 100644
--- a/iris/algebra/namespace_map.v
+++ b/iris/algebra/namespace_map.v
@@ -91,7 +91,7 @@ Proof. intros. apply NamespaceMap_discrete; apply _. Qed.
 Global Instance namespace_map_token_discrete E : Discrete (@namespace_map_token A E).
 Proof. intros. apply NamespaceMap_discrete; apply _. Qed.
 
-Local Instance namespace_map_valid : Valid (namespace_map A) := λ x,
+Local Instance namespace_map_valid_instance : Valid (namespace_map A) := λ x,
   match namespace_map_token_proj x with
   | CoPset E =>
      ✓ (namespace_map_data_proj x) ∧
@@ -99,8 +99,8 @@ Local Instance namespace_map_valid : Valid (namespace_map A) := λ x,
      ∀ i, namespace_map_data_proj x !! i = None ∨ i ∉ E
   | CoPsetBot => False
   end.
-Global Arguments namespace_map_valid !_ /.
-Local Instance namespace_map_validN : ValidN (namespace_map A) := λ n x,
+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 =>
      ✓{n} (namespace_map_data_proj x) ∧
@@ -108,10 +108,10 @@ Local Instance namespace_map_validN : ValidN (namespace_map A) := λ n x,
      ∀ i, namespace_map_data_proj x !! i = None ∨ i ∉ E
   | CoPsetBot => False
   end.
-Global Arguments namespace_map_validN !_ /.
-Local Instance namespace_map_pcore : PCore (namespace_map A) := λ x,
+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 : Op (namespace_map A) := λ x y,
+Local Instance namespace_map_op_instance : Op (namespace_map A) := λ x y,
   NamespaceMap (namespace_map_data_proj x â‹… namespace_map_data_proj y)
                (namespace_map_token_proj x â‹… namespace_map_token_proj y).
 
@@ -193,7 +193,7 @@ Proof.
   by intros [?%cmra_discrete_valid ?].
 Qed.
 
-Local Instance namespace_map_empty : Unit (namespace_map A) := NamespaceMap ε ε.
+Local Instance namespace_map_empty_instance : Unit (namespace_map A) := NamespaceMap ε ε.
 Lemma namespace_map_ucmra_mixin : UcmraMixin (namespace_map A).
 Proof.
   split; simpl.
@@ -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 14b02b9dfa9abe703fcb802bf7e71f04db91d92f..c03951ac55f1a6da4a69aad38c6f6d2f9200e32e 100644
--- a/iris/algebra/numbers.v
+++ b/iris/algebra/numbers.v
@@ -3,10 +3,10 @@ From iris.prelude Require Import options.
 
 (** ** Natural numbers with [add] as the operation. *)
 Section nat.
-  Local Instance nat_valid : Valid nat := λ x, True.
-  Local Instance nat_validN : ValidN nat := λ n x, True.
-  Local Instance nat_pcore : PCore nat := λ x, Some 0.
-  Local Instance nat_op : Op nat := plus.
+  Local Instance nat_valid_instance : Valid nat := λ x, True.
+  Local Instance nat_validN_instance : ValidN nat := λ n x, True.
+  Local Instance nat_pcore_instance : PCore nat := λ x, Some 0.
+  Local Instance nat_op_instance : Op nat := plus.
   Definition nat_op_plus x y : x â‹… y = x + y := eq_refl.
   Lemma nat_included (x y : nat) : x ≼ y ↔ x ≤ y.
   Proof. by rewrite nat_le_sum. Qed.
@@ -23,7 +23,7 @@ Section nat.
   Global Instance nat_cmra_discrete : CmraDiscrete natR.
   Proof. apply discrete_cmra_discrete. Qed.
 
-  Local Instance nat_unit : Unit nat := 0.
+  Local Instance nat_unit_instance : Unit nat := 0.
   Lemma nat_ucmra_mixin : UcmraMixin nat.
   Proof. split; apply _ || done. Qed.
   Canonical Structure natUR : ucmra := Ucmra nat nat_ucmra_mixin.
@@ -51,18 +51,18 @@ Add Printing Constructor max_nat.
 Canonical Structure max_natO := leibnizO max_nat.
 
 Section max_nat.
-  Local Instance max_nat_unit : Unit max_nat := MaxNat 0.
-  Local Instance max_nat_valid : Valid max_nat := λ x, True.
-  Local Instance max_nat_validN : ValidN max_nat := λ n x, True.
-  Local Instance max_nat_pcore : PCore max_nat := Some.
-  Local Instance max_nat_op : Op max_nat := λ n m, MaxNat (max_nat_car n `max` max_nat_car m).
+  Local Instance max_nat_unit_instance : Unit max_nat := MaxNat 0.
+  Local Instance max_nat_valid_instance : Valid max_nat := λ x, True.
+  Local Instance max_nat_validN_instance : ValidN max_nat := λ n x, True.
+  Local Instance max_nat_pcore_instance : PCore max_nat := Some.
+  Local Instance max_nat_op_instance : Op max_nat := λ n m, MaxNat (max_nat_car n `max` max_nat_car m).
   Definition max_nat_op_max x y : MaxNat x â‹… MaxNat y = MaxNat (x `max` y) := eq_refl.
 
   Lemma max_nat_included x y : x ≼ y ↔ max_nat_car x ≤ max_nat_car y.
   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.
@@ -107,17 +107,17 @@ Add Printing Constructor min_nat.
 Canonical Structure min_natO := leibnizO min_nat.
 
 Section min_nat.
-  Local Instance min_nat_valid : Valid min_nat := λ x, True.
-  Local Instance min_nat_validN : ValidN min_nat := λ n x, True.
-  Local Instance min_nat_pcore : PCore min_nat := Some.
-  Local Instance min_nat_op : Op min_nat := λ n m, MinNat (min_nat_car n `min` min_nat_car m).
+  Local Instance min_nat_valid_instance : Valid min_nat := λ x, True.
+  Local Instance min_nat_validN_instance : ValidN min_nat := λ n x, True.
+  Local Instance min_nat_pcore_instance : PCore min_nat := Some.
+  Local Instance min_nat_op_instance : Op min_nat := λ n m, MinNat (min_nat_car n `min` min_nat_car m).
   Definition min_nat_op_min x y : MinNat x â‹… MinNat y = MinNat (x `min` y) := eq_refl.
 
   Lemma min_nat_included (x y : min_nat) : x ≼ y ↔ min_nat_car y ≤ min_nat_car x.
   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.
@@ -159,10 +159,10 @@ End min_nat.
 
 (** ** Positive integers with [Pos.add] as the operation. *)
 Section positive.
-  Local Instance pos_valid : Valid positive := λ x, True.
-  Local Instance pos_validN : ValidN positive := λ n x, True.
-  Local Instance pos_pcore : PCore positive := λ x, None.
-  Local Instance pos_op : Op positive := Pos.add.
+  Local Instance pos_valid_instance : Valid positive := λ x, True.
+  Local Instance pos_validN_instance : ValidN positive := λ n x, True.
+  Local Instance pos_pcore_instance : PCore positive := λ x, None.
+  Local Instance pos_op_instance : Op positive := Pos.add.
   Definition pos_op_plus x y : x â‹… y = (x + y)%positive := eq_refl.
   Lemma pos_included (x y : positive) : x ≼ y ↔ (x < y)%positive.
   Proof. by rewrite Plt_sum. Qed.
diff --git a/iris/algebra/sts.v b/iris/algebra/sts.v
index 707deaecee218a2a20440cb393288303cd2890ba..bac537bb9b322b64dc4e21620a818c0366c93ce3 100644
--- a/iris/algebra/sts.v
+++ b/iris/algebra/sts.v
@@ -197,12 +197,12 @@ Inductive sts_equiv : Equiv (car sts) :=
   | auth_equiv s T1 T2 : T1 ≡ T2 → auth s T1 ≡ auth s T2
   | frag_equiv S1 S2 T1 T2 : T1 ≡ T2 → S1 ≡ S2 → frag S1 T1 ≡ frag S2 T2.
 Existing Instance sts_equiv.
-Local Instance sts_valid : Valid (car sts) := λ x,
+Local Instance sts_valid_instance : Valid (car sts) := λ x,
   match x with
   | auth s T => tok s ## T
   | frag S' T => closed S' T ∧ ∃ s, s ∈ S'
   end.
-Local Instance sts_core : PCore (car sts) := λ x,
+Local Instance sts_core_instance : PCore (car sts) := λ x,
   Some match x with
   | frag S' _ => frag (up_set S' ∅ ) ∅
   | auth s _  => frag (up s ∅) ∅
@@ -213,7 +213,7 @@ Inductive sts_disjoint : Disjoint (car sts) :=
   | auth_frag_disjoint s S T1 T2 : s ∈ S → T1 ## T2 → auth s T1 ## frag S T2
   | frag_auth_disjoint s S T1 T2 : s ∈ S → T1 ## T2 → frag S T1 ## auth s T2.
 Existing Instance sts_disjoint.
-Local Instance sts_op : Op (car sts) := λ x1 x2,
+Local Instance sts_op_instance : Op (car sts) := λ x1 x2,
   match x1, x2 with
   | frag S1 T1, frag S2 T2 => frag (S1 ∩ S2) (T1 ∪ T2)
   | auth s T1, frag _ T2 => auth s (T1 ∪ T2)
diff --git a/iris/algebra/ufrac.v b/iris/algebra/ufrac.v
index 821fc4ceba0ada6f7e5644beac71a630aa3356d1..144646382b3ba4864baf47b675733030a348c140 100644
--- a/iris/algebra/ufrac.v
+++ b/iris/algebra/ufrac.v
@@ -14,9 +14,9 @@ Section ufrac.
 
   Canonical Structure ufracO := leibnizO ufrac.
 
-  Local Instance ufrac_valid : Valid ufrac := λ x, True.
-  Local Instance ufrac_pcore : PCore ufrac := λ _, None.
-  Local Instance ufrac_op : Op ufrac := λ x y, (x + y)%Qp.
+  Local Instance ufrac_valid_instance : Valid ufrac := λ x, True.
+  Local Instance ufrac_pcore_instance : PCore ufrac := λ _, None.
+  Local Instance ufrac_op_instance : Op ufrac := λ x y, (x + y)%Qp.
 
   Lemma ufrac_op' p q : p â‹… q = (p + q)%Qp.
   Proof. done. Qed.
diff --git a/iris/algebra/view.v b/iris/algebra/view.v
index 976034e1e85dfe6cb34c82b693b81ee177368b64..9989cafd4bf67e9651a866021084c42ce8a0464f 100644
--- a/iris/algebra/view.v
+++ b/iris/algebra/view.v
@@ -173,21 +173,21 @@ Section cmra.
   Global Instance view_frag_inj : Inj (≡) (≡) (@view_frag A B rel).
   Proof. by intros ?? [??]. Qed.
 
-  Local Instance view_valid : Valid (view rel) := λ x,
+  Local Instance view_valid_instance : Valid (view rel) := λ x,
     match view_auth_proj x with
     | Some (q, ag) =>
        ✓ q ∧ (∀ n, ∃ a, ag ≡{n}≡ to_agree a ∧ rel n a (view_frag_proj x))
     | None => ∀ n, ∃ a, rel n a (view_frag_proj x)
     end.
-  Local Instance view_validN : ValidN (view rel) := λ n x,
+  Local Instance view_validN_instance : ValidN (view rel) := λ n x,
     match view_auth_proj x with
     | Some (q, ag) =>
        ✓{n} q ∧ ∃ a, ag ≡{n}≡ to_agree a ∧ rel n a (view_frag_proj x)
     | None => ∃ a, rel n a (view_frag_proj x)
     end.
-  Local Instance view_pcore : PCore (view rel) := λ x,
+  Local Instance view_pcore_instance : PCore (view rel) := λ x,
     Some (View (core (view_auth_proj x)) (core (view_frag_proj x))).
-  Local Instance view_op : Op (view rel) := λ x y,
+  Local Instance view_op_instance : Op (view rel) := λ x y,
     View (view_auth_proj x â‹… view_auth_proj y) (view_frag_proj x â‹… view_frag_proj y).
 
   Local Definition view_valid_eq :
@@ -253,7 +253,7 @@ Section cmra.
     - naive_solver.
   Qed.
 
-  Local Instance view_empty : Unit (view rel) := View ε ε.
+  Local Instance view_empty_instance : Unit (view rel) := View ε ε.
   Lemma view_ucmra_mixin : UcmraMixin (view rel).
   Proof.
     split; simpl.
@@ -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.