diff --git a/Makefile.coq.local b/Makefile.coq.local
index 6a0bc865635542d7b1864c6c811bee0ad6220df1..f87fa5779ea71bb814c26bbf9e8e94e0bb1be4a0 100644
--- a/Makefile.coq.local
+++ b/Makefile.coq.local
@@ -16,7 +16,7 @@ test: $(TESTFILES:.v=.vo)
 	$(SHOW)"Performing some style checks..."
 	$(HIDE)for FILE in $(VFILES); do \
 	  if ! fgrep -q 'From iris.prelude Require Import options.' "$$FILE"; then echo "ERROR: $$FILE does not import 'options'."; echo; exit 1; fi ; \
-	  if egrep '^\s*(Instance|Arguments|Remove|Hint\s+(Extern|Constructors|Resolve|Immediate|Mode|Opaque|Transparent|Unfold)|(Open|Close)\s+Scope)\s' "$$FILE"; then echo "ERROR: $$FILE contains unqualified 'Instance'/'Arguments'/'Hint'/'Scope' (see above)."; echo "Please add 'Global' or 'Local' as appropriate."; echo; exit 1; fi \
+	  if egrep -n '^\s*((Existing\s+|Program\s+)Instance|Arguments|Remove|Hint\s+(Extern|Constructors|Resolve|Immediate|Mode|Opaque|Transparent|Unfold)|(Open|Close)\s+Scope)\b' "$$FILE"; then echo "ERROR: $$FILE contains unqualified 'Instance'/'Arguments'/'Hint'/'Scope' (see above)."; echo "Please add 'Global' or 'Local' as appropriate."; echo; exit 1; fi \
 	done
 # Make sure main Iris does not import other Iris packages.
 	$(HIDE)if egrep 'iris\.(heap_lang|deprecated|staging)' --include "*.v" -R iris; then echo "ERROR: Iris may not import modules from other Iris packages (see above for violations)."; echo; exit 1; fi
diff --git a/iris/algebra/agree.v b/iris/algebra/agree.v
index 66bd3e41428ae432b82effa03540fe5f3c08ce81..2421f83326bf2b050df89b330ad6a21012ae5bec 100644
--- a/iris/algebra/agree.v
+++ b/iris/algebra/agree.v
@@ -86,7 +86,7 @@ Local Instance agree_validN_instance : ValidN (agree A) := λ n x,
   end.
 Local Instance agree_valid_instance : Valid (agree A) := λ x, ∀ n, ✓{n} x.
 
-Program Instance agree_op_instance : Op (agree A) := λ x y,
+Local 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_instance : PCore (agree A) := Some.
diff --git a/iris/algebra/cmra.v b/iris/algebra/cmra.v
index 8c9ca92f21ee1ce65266763134da0603ea3c4bcb..43a8a068c5b930af446bf568119716af392e9831 100644
--- a/iris/algebra/cmra.v
+++ b/iris/algebra/cmra.v
@@ -795,7 +795,7 @@ Record rFunctor := RFunctor {
       (fg : (A2 -n> A1) * (B1 -n> B2)) :
     CmraMorphism (rFunctor_map fg)
 }.
-Existing Instances rFunctor_map_ne rFunctor_mor.
+Global Existing Instances rFunctor_map_ne rFunctor_mor.
 Global Instance: Params (@rFunctor_map) 9 := {}.
 
 Declare Scope rFunctor_scope.
@@ -886,7 +886,7 @@ Record urFunctor := URFunctor {
       (fg : (A2 -n> A1) * (B1 -n> B2)) :
     CmraMorphism (urFunctor_map fg)
 }.
-Existing Instances urFunctor_map_ne urFunctor_mor.
+Global Existing Instances urFunctor_map_ne urFunctor_mor.
 Global Instance: Params (@urFunctor_map) 9 := {}.
 
 Declare Scope urFunctor_scope.
diff --git a/iris/algebra/cofe_solver.v b/iris/algebra/cofe_solver.v
index 69fea25714e541dac0d38fb8a85bace43ed48459..f2b452fe9cd6334cf4a4ba3563d6389b084c230c 100644
--- a/iris/algebra/cofe_solver.v
+++ b/iris/algebra/cofe_solver.v
@@ -6,7 +6,7 @@ Record solution (F : oFunctor) := Solution {
   solution_cofe : Cofe solution_car;
   solution_iso :> ofe_iso (oFunctor_apply F solution_car) solution_car;
 }.
-Existing Instance solution_cofe.
+Global Existing Instance solution_cofe.
 
 Module solver. Section solver.
 Context (F : oFunctor) `{Fcontr : oFunctorContractive F}.
diff --git a/iris/algebra/csum.v b/iris/algebra/csum.v
index 2d55fd1e3c6ca73752a8b25720262034bf2b6805..28209dfb804fe2f82fb4df04b465a3e8db63d276 100644
--- a/iris/algebra/csum.v
+++ b/iris/algebra/csum.v
@@ -36,12 +36,12 @@ Inductive csum_equiv : Equiv (csum A B) :=
   | Cinl_equiv a a' : a ≡ a' → Cinl a ≡ Cinl a'
   | Cinr_equiv b b' : b ≡ b' → Cinr b ≡ Cinr b'
   | CsumBot_equiv : CsumBot ≡ CsumBot.
-Existing Instance csum_equiv.
+Local Existing Instance csum_equiv.
 Inductive csum_dist : Dist (csum A B) :=
   | Cinl_dist n a a' : a ≡{n}≡ a' → Cinl a ≡{n}≡ Cinl a'
   | Cinr_dist n b b' : b ≡{n}≡ b' → Cinr b ≡{n}≡ Cinr b'
   | CsumBot_dist n : CsumBot ≡{n}≡ CsumBot.
-Existing Instance csum_dist.
+Local Existing Instance csum_dist.
 
 Global Instance Cinl_ne : NonExpansive (@Cinl A B).
 Proof. by constructor. Qed.
diff --git a/iris/algebra/dra.v b/iris/algebra/dra.v
index b2b7ae2012c20ecb9796f8aa489baf75e6e4a260..01ed39ecf09abe6756764e625e98536b0a813f65 100644
--- a/iris/algebra/dra.v
+++ b/iris/algebra/dra.v
@@ -44,7 +44,7 @@ Global Arguments dra_op : simpl never.
 Global Arguments dra_valid : simpl never.
 Global Arguments dra_mixin : simpl never.
 Add Printing Constructor draT.
-Existing Instances dra_equiv dra_pcore dra_disjoint dra_op dra_valid.
+Global Existing Instances dra_equiv dra_pcore dra_disjoint dra_op dra_valid.
 
 (** Lifting properties from the mixin *)
 Section dra_mixin.
@@ -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_instance : PCore (validity A) := λ x,
+Local 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_instance : Op (validity A) := λ x y,
+Local 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 0dec359fbf0aa0cde084bcaa26672a78c4029676..54646d39061617ee363302fe07098796b069f2fa 100644
--- a/iris/algebra/excl.v
+++ b/iris/algebra/excl.v
@@ -29,11 +29,11 @@ Implicit Types x y : excl A.
 Inductive excl_equiv : Equiv (excl A) :=
   | Excl_equiv a b : a ≡ b → Excl a ≡ Excl b
   | ExclBot_equiv : ExclBot ≡ ExclBot.
-Existing Instance excl_equiv.
+Local Existing Instance excl_equiv.
 Inductive excl_dist : Dist (excl A) :=
   | Excl_dist a b n : a ≡{n}≡ b → Excl a ≡{n}≡ Excl b
   | ExclBot_dist n : ExclBot ≡{n}≡ ExclBot.
-Existing Instance excl_dist.
+Local Existing Instance excl_dist.
 
 Global Instance Excl_ne : NonExpansive (@Excl A).
 Proof. by constructor. Qed.
diff --git a/iris/algebra/ofe.v b/iris/algebra/ofe.v
index 01cbd49d8ccf81ab50eacb90339508c2019c9407..d743539a62c1e7b8833e8c1e86c354fbc58a010b 100644
--- a/iris/algebra/ofe.v
+++ b/iris/algebra/ofe.v
@@ -535,7 +535,7 @@ Record ofe_mor (A B : ofe) : Type := OfeMor {
 }.
 Global Arguments OfeMor {_ _} _ {_}.
 Add Printing Constructor ofe_mor.
-Existing Instance ofe_mor_ne.
+Global Existing Instance ofe_mor_ne.
 
 Notation "'λne' x .. y , t" :=
   (@OfeMor _ _ (λ x, .. (@OfeMor _ _ (λ y, t) _) ..) _)
@@ -710,7 +710,7 @@ Record oFunctor := OFunctor {
       (f : A2 -n> A1) (g : A3 -n> A2) (f' : B1 -n> B2) (g' : B2 -n> B3) x :
     oFunctor_map (f◎g, g'◎f') x ≡ oFunctor_map (g,g') (oFunctor_map (f,f') x)
 }.
-Existing Instance oFunctor_map_ne.
+Global Existing Instance oFunctor_map_ne.
 Global Instance: Params (@oFunctor_map) 9 := {}.
 
 Declare Scope oFunctor_scope.
@@ -1329,7 +1329,7 @@ Section iso_cofe_subtype.
   Context (g_dist : ∀ n y1 y2, y1 ≡{n}≡ y2 ↔ g y1 ≡{n}≡ g y2).
   Let Hgne : NonExpansive g.
   Proof. intros n y1 y2. apply g_dist. Qed.
-  Existing Instance Hgne.
+  Local Existing Instance Hgne.
   Context (gf : ∀ x Hx, g (f x Hx) ≡ x).
   Context (Hlimit : ∀ c : chain B, P (compl (chain_map g c))).
   Program Definition iso_cofe_subtype : Cofe B :=
diff --git a/iris/algebra/proofmode_classes.v b/iris/algebra/proofmode_classes.v
index 41571ba257a8d1f046cfb4ee930121c0bacc826a..489a9e36c8428947fdf12b7b2248435f4bb12a56 100644
--- a/iris/algebra/proofmode_classes.v
+++ b/iris/algebra/proofmode_classes.v
@@ -27,7 +27,7 @@ Global Hint Mode IsOp' + ! - - : typeclass_instances.
 Global Hint Mode IsOp' + - ! ! : typeclass_instances.
 
 Class IsOp'LR {A : cmra} (a b1 b2 : A) := is_op_lr : IsOp a b1 b2.
-Existing Instance is_op_lr | 0.
+Global Existing Instance is_op_lr | 0.
 Global Hint Mode IsOp'LR + ! - - : typeclass_instances.
 Global Instance is_op_lr_op {A : cmra} (a b : A) : IsOp'LR (a â‹… b) a b | 0.
 Proof. by rewrite /IsOp'LR /IsOp. Qed.
diff --git a/iris/algebra/sts.v b/iris/algebra/sts.v
index 06c86aaf2aa23f327f8c8e236c616e6713b773c2..88b8cba6e743f4ed1ac13ad5cf54130e12c8a31f 100644
--- a/iris/algebra/sts.v
+++ b/iris/algebra/sts.v
@@ -196,7 +196,7 @@ Implicit Types T : tokens sts.
 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 Existing Instance sts_equiv.
 Local Instance sts_valid_instance : Valid (car sts) := λ x,
   match x with
   | auth s T => tok s ## T
@@ -212,7 +212,7 @@ Inductive sts_disjoint : Disjoint (car sts) :=
      (∃ s, s ∈ S1 ∩ S2) → T1 ## T2 → frag S1 T1 ## frag S2 T2
   | 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 Existing Instance sts_disjoint.
 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)
diff --git a/iris/base_logic/lib/iprop.v b/iris/base_logic/lib/iprop.v
index bccdb42bfaa8687af567b081ba9f09ff021fb7c5..1b2c47ce18e53e697a1e0701e1bb4f1419178085 100644
--- a/iris/base_logic/lib/iprop.v
+++ b/iris/base_logic/lib/iprop.v
@@ -29,7 +29,7 @@ Structure gFunctor := GFunctor {
   gFunctor_map_contractive : rFunctorContractive gFunctor_F;
 }.
 Global Arguments GFunctor _ {_}.
-Existing Instance gFunctor_map_contractive.
+Global Existing Instance gFunctor_map_contractive.
 Add Printing Constructor gFunctor.
 
 (** The type [gFunctors] describes the parameters [Σ] of the Iris logic: lists
diff --git a/iris/bi/derived_connectives.v b/iris/bi/derived_connectives.v
index 0027f0f0de366556f78da609584e52ce856abd12..7f965854e1f601170fe9466928ab295fb8af51b8 100644
--- a/iris/bi/derived_connectives.v
+++ b/iris/bi/derived_connectives.v
@@ -32,7 +32,7 @@ Global Hint Mode Affine + ! : typeclass_instances.
 
 Class BiAffine (PROP : bi) := absorbing_bi (Q : PROP) : Affine Q.
 Global Hint Mode BiAffine ! : typeclass_instances.
-Existing Instance absorbing_bi | 0.
+Global Existing Instance absorbing_bi | 0.
 
 Class BiPositive (PROP : bi) :=
   bi_positive (P Q : PROP) : <affine> (P ∗ Q) ⊢ <affine> P ∗ Q.
diff --git a/iris/bi/monpred.v b/iris/bi/monpred.v
index 30f159eb83b8076f79b645d524e04c7f69dc7c19..afda962f8adbee876777e572826d32734cb87d84 100644
--- a/iris/bi/monpred.v
+++ b/iris/bi/monpred.v
@@ -9,7 +9,7 @@ Structure biIndex :=
       bi_index_inhabited : Inhabited bi_index_type;
       bi_index_rel : SqSubsetEq bi_index_type;
       bi_index_rel_preorder : PreOrder (⊑@{bi_index_type}) }.
-Existing Instances bi_index_inhabited bi_index_rel bi_index_rel_preorder.
+Global Existing Instances bi_index_inhabited bi_index_rel bi_index_rel_preorder.
 
 (* We may want to instantiate monPred with the reflexivity relation in
    the case where there is no relevent order. In that case, there is
diff --git a/iris/program_logic/total_weakestpre.v b/iris/program_logic/total_weakestpre.v
index f2fd5b3e1c16549a92d1431335726e7283d1c18a..8b98e91aee33b04f062fd898da0f6e543565696b 100644
--- a/iris/program_logic/total_weakestpre.v
+++ b/iris/program_logic/total_weakestpre.v
@@ -62,7 +62,7 @@ Definition twp_def `{!irisG Λ Σ} : Twp Λ (iProp Σ) stuckness
 Definition twp_aux : seal (@twp_def). Proof. by eexists. Qed.
 Definition twp' := twp_aux.(unseal).
 Global Arguments twp' {Λ Σ _}.
-Existing Instance twp'.
+Global Existing Instance twp'.
 Lemma twp_eq `{!irisG Λ Σ} : twp = @twp_def Λ Σ _.
 Proof. rewrite -twp_aux.(seal_eq) //. Qed.
 
diff --git a/iris/program_logic/weakestpre.v b/iris/program_logic/weakestpre.v
index 883d401af9e682b85437a556ca9c76d7b43c3e4f..e3656a5dd934e7c3c4214d62465e1fb54467dfc5 100644
--- a/iris/program_logic/weakestpre.v
+++ b/iris/program_logic/weakestpre.v
@@ -78,7 +78,7 @@ Definition wp_def `{!irisG Λ Σ} : Wp Λ (iProp Σ) stuckness :=
 Definition wp_aux : seal (@wp_def). Proof. by eexists. Qed.
 Definition wp' := wp_aux.(unseal).
 Global Arguments wp' {Λ Σ _}.
-Existing Instance wp'.
+Global Existing Instance wp'.
 Lemma wp_eq `{!irisG Λ Σ} : wp = @wp_def Λ Σ _.
 Proof. rewrite -wp_aux.(seal_eq) //. Qed.
 
diff --git a/iris/proofmode/classes.v b/iris/proofmode/classes.v
index a57e644d8273ca106d8ec72e67e6a12e92c66375..88bf16a4a42cf74c6a6fe82fb785d1aa1ca69827 100644
--- a/iris/proofmode/classes.v
+++ b/iris/proofmode/classes.v
@@ -512,7 +512,7 @@ Global Arguments AsEmpValid {_} _%type _%I.
 Class AsEmpValid0 {PROP : bi} (φ : Prop) (P : PROP) :=
   as_emp_valid_0 : AsEmpValid φ P.
 Global Arguments AsEmpValid0 {_} _%type _%I.
-Existing Instance as_emp_valid_0 | 0.
+Global Existing Instance as_emp_valid_0 | 0.
 
 Lemma as_emp_valid_1 (φ : Prop) {PROP : bi} (P : PROP) `{!AsEmpValid φ P} :
   φ → ⊢ P.
@@ -570,7 +570,7 @@ Global Hint Mode IntoAcc + - ! - - - - - - - : typeclass_instances.
 
 (* The typeclass used for the [iInv] tactic.
    Input: [Pinv]
-   Arguments:
+   Other Arguments:
    - [Pinv] is an invariant assertion
    - [Pin] is an additional logic assertion needed for opening an invariant
    - [φ] is an additional Coq assertion needed for opening an invariant
diff --git a/iris/proofmode/coq_tactics.v b/iris/proofmode/coq_tactics.v
index 617d76f436a64cbaff56b0d98fd781d8bcfb1d46..a2c2007f351ad895561e830577cd642387e97d37 100644
--- a/iris/proofmode/coq_tactics.v
+++ b/iris/proofmode/coq_tactics.v
@@ -931,7 +931,7 @@ Inductive IntoModalIntuitionisticEnv {PROP2} : ∀ {PROP1} (M : modality PROP1 P
   | MIEnvId_intuitionistic (M : modality PROP2 PROP2) Γ :
      IntoModalIntuitionisticEnv M Γ Γ MIEnvId.
 Existing Class IntoModalIntuitionisticEnv.
-Existing Instances MIEnvIsEmpty_intuitionistic MIEnvForall_intuitionistic
+Global Existing Instances MIEnvIsEmpty_intuitionistic MIEnvForall_intuitionistic
   MIEnvTransform_intuitionistic MIEnvClear_intuitionistic MIEnvId_intuitionistic.
 
 (* The class [IntoModalSpatialEnv M Γin Γout s] is used to transform the spatial
@@ -963,7 +963,7 @@ Inductive IntoModalSpatialEnv {PROP2} : ∀ {PROP1} (M : modality PROP1 PROP2)
   | MIEnvId_spatial (M : modality PROP2 PROP2) Γ :
      IntoModalSpatialEnv M Γ Γ MIEnvId false.
 Existing Class IntoModalSpatialEnv.
-Existing Instances MIEnvIsEmpty_spatial MIEnvForall_spatial
+Global Existing Instances MIEnvIsEmpty_spatial MIEnvForall_spatial
   MIEnvTransform_spatial MIEnvClear_spatial MIEnvId_spatial.
 
 Section tac_modal_intro.
diff --git a/iris_heap_lang/lib/increment.v b/iris_heap_lang/lib/increment.v
index 0fdee4cd0327ae37ce5dc13657f486146e8898ac..4887a01cc0b59aa2fa7c613672c7fb02d0e4cdb0 100644
--- a/iris_heap_lang/lib/increment.v
+++ b/iris_heap_lang/lib/increment.v
@@ -147,7 +147,7 @@ End increment.
 Section increment_client.
   Context `{!heapG Σ, !spawnG Σ}.
 
-  Existing Instance primitive_atomic_heap.
+  Local Existing Instance primitive_atomic_heap.
 
   Definition incr_client : val :=
     λ: "x",
diff --git a/iris_heap_lang/lib/lock.v b/iris_heap_lang/lib/lock.v
index 1b0414e64d6466fd6c68151103ec2e4f2f3864d9..bc7d88da8bb916c571b76c39af1e42665da13af1 100644
--- a/iris_heap_lang/lib/lock.v
+++ b/iris_heap_lang/lib/lock.v
@@ -36,7 +36,7 @@ Global Arguments release {_ _} _.
 Global Arguments is_lock {_ _} _ _ _ _.
 Global Arguments locked {_ _} _ _.
 
-Existing Instances is_lock_ne is_lock_persistent locked_timeless.
+Global Existing Instances is_lock_ne is_lock_persistent locked_timeless.
 
 Global Instance is_lock_proper Σ `{!heapG Σ} (L: lock Σ) γ lk:
   Proper ((≡) ==> (≡)) (is_lock L γ lk) := ne_proper _.
diff --git a/iris_heap_lang/locations.v b/iris_heap_lang/locations.v
index aae2090d1b2a3cb133b6bbf787d81137b6a6ea2a..a11775e143c23b4ad3150e8c3699f67c1893bb8e 100644
--- a/iris_heap_lang/locations.v
+++ b/iris_heap_lang/locations.v
@@ -14,7 +14,7 @@ Global Instance loc_inhabited : Inhabited loc := populate {|loc_car := 0 |}.
 Global Instance loc_countable : Countable loc.
 Proof. by apply (inj_countable' loc_car Loc); intros []. Defined.
 
-Program Instance loc_infinite : Infinite loc :=
+Global Program Instance loc_infinite : Infinite loc :=
   inj_infinite (λ p, {| loc_car := p |}) (λ l, Some (loc_car l)) _.
 Next Obligation. done. Qed.
 
diff --git a/iris_staging/algebra/max_prefix_list.v b/iris_staging/algebra/max_prefix_list.v
index 715bfac4c45b6b7fbea7051b3590b78e9d207a47..ec1b0c2af1789deff3a2009fc745932565a01679 100644
--- a/iris_staging/algebra/max_prefix_list.v
+++ b/iris_staging/algebra/max_prefix_list.v
@@ -11,7 +11,7 @@ Definition max_prefix_listUR (A : ofe) := gmapUR nat (agreeR A).
 
 Definition to_max_prefix_list {A} (l : list A) : gmap nat (agree A) :=
   to_agree <$> map_seq 0 l.
-Instance: Params (@to_max_prefix_list) 1 := {}.
+Global Instance: Params (@to_max_prefix_list) 1 := {}.
 Typeclasses Opaque to_max_prefix_list.
 
 Section max_prefix_list.
diff --git a/iris_staging/algebra/mono_list.v b/iris_staging/algebra/mono_list.v
index 7954fa9fbc16e6ff10211cdbe1b90f4e91f6f9f7..a417154510c453990964eee1305c82dcb02d4487 100644
--- a/iris_staging/algebra/mono_list.v
+++ b/iris_staging/algebra/mono_list.v
@@ -17,8 +17,8 @@ Definition mono_list_auth {A : ofe} (q : dfrac) (l : list A) : mono_listR A :=
   ●{q} (to_max_prefix_list l) ⋅ ◯ (to_max_prefix_list l).
 Definition mono_list_lb {A : ofe} (l : list A) : mono_listR A :=
   â—¯ (to_max_prefix_list l).
-Instance: Params (@mono_list_auth) 2 := {}.
-Instance: Params (@mono_list_lb) 1 := {}.
+Global Instance: Params (@mono_list_auth) 2 := {}.
+Global Instance: Params (@mono_list_lb) 1 := {}.
 Typeclasses Opaque mono_list_auth mono_list_lb.
 
 (** FIXME: Refactor these notations using custom entries once Coq bug #13654