diff --git a/iris/algebra/agree.v b/iris/algebra/agree.v
index 089456dee685d5e12f3b3ce3bbaf369b8c0b1490..faf3437c2166fd464182b8de2f280da02c5e98bb 100644
--- a/iris/algebra/agree.v
+++ b/iris/algebra/agree.v
@@ -79,17 +79,17 @@ 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.
diff --git a/iris/algebra/cmra.v b/iris/algebra/cmra.v
index 5ba38dff3b960267a4114a989cee78d81329be15..2f74c62b8071c6aa4baa59b07ad6e7f9850d0262 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 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).
@@ -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 Instance option_pcore_instance : 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_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 _.
@@ -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,10 +1597,10 @@ 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.
@@ -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..b18d881119958f11d9460aaf7e7055b57f7212c3 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
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..6b4c8d6974ba8f44616f7fbc6c02716b77aebdf2 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.
@@ -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..20674cd1603619495f8ab1829e6e441d1162b71d 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) ∧
@@ -100,7 +100,7 @@ Local Instance namespace_map_valid : Valid (namespace_map A) := λ x,
   | CoPsetBot => False
   end.
 Global Arguments namespace_map_valid !_ /.
-Local Instance namespace_map_validN : ValidN (namespace_map A) := λ n x,
+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) ∧
@@ -109,9 +109,9 @@ Local Instance namespace_map_validN : ValidN (namespace_map A) := λ n x,
   | CoPsetBot => False
   end.
 Global Arguments namespace_map_validN !_ /.
-Local Instance namespace_map_pcore : PCore (namespace_map A) := λ x,
+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.
diff --git a/iris/algebra/numbers.v b/iris/algebra/numbers.v
index 14b02b9dfa9abe703fcb802bf7e71f04db91d92f..5d778a4a2cd7772ae6c0114cbd1885ed9dc58401 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,11 +51,11 @@ 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.
@@ -107,10 +107,10 @@ 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.
@@ -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..09f306b3a8c4b086a6eb0b090dd239a743cc7445 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.