diff --git a/CHANGELOG.md b/CHANGELOG.md
index 81e65e0efbaac527adc9df29866523b2fd03f23b..712c4b8a2ab92ff96387d676d4c5c6c72cc8291a 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -6,7 +6,8 @@ API-breaking change is listed.
 Coq 8.11 is no longer supported.
 
 - Make sure that `gset` and `mapset` do not bump the universe.
-- Rewrite `tele_arg` to make it not bump universes. (by Gregory Malecha, BedRock Systems)
+- Rewrite `tele_arg` to make it not bump universes. (by Gregory Malecha, BedRock
+  Systems)
 - Change `dom D M` (where `D` is the domain type) to `dom M`; the domain type is
   now inferred automatically. To make this possible, getting the domain of a
   `gmap` as a `coGset` and of a `Pmap` as a `coPset` is no longer supported. Use
@@ -14,6 +15,9 @@ Coq 8.11 is no longer supported.
   When combining `dom` with `≡`, this can run into an old issue (due to a Coq
   issue, `Equiv` does not the desired `Hint Mode !`), which can make it
   necessary to annotate the set type at the `≡` via `≡@{D}`.
+- Rename "unsealing" lemmas from `_eq` to `_unseal`. This affects `ndot_eq` and
+  `nclose_eq`. These unsealing lemmas are internal, so in principle you should
+  not rely on them.
 
 ## std++ 1.7.0 (2022-01-22)
 
diff --git a/theories/base.v b/theories/base.v
index 010b34e610c46dc39aae5451433c6051ebd28581..a09cd676ff7b92e32dd709ab3e11fa3df9047aba 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -46,8 +46,10 @@ introduces all variables and gives them fresh names. As such, it becomes
 impossible to refer to hypotheses in a robust way. *)
 Obligation Tactic := idtac.
 
-(** 3. Hide obligations from the results of the [Search] commands. *)
+(** 3. Hide obligations and unsealing lemmas from the results of the [Search]
+commands. *)
 Add Search Blacklist "_obligation_".
+Add Search Blacklist "_unseal".
 
 (** * Sealing off definitions *)
 Section seal.
diff --git a/theories/namespaces.v b/theories/namespaces.v
index 975d7f48fd73448c7e453b7e33b0b4bc58adc4f6..e6f878de03a6e630ab071309747e2729f3e535c1 100644
--- a/theories/namespaces.v
+++ b/theories/namespaces.v
@@ -8,17 +8,17 @@ Typeclasses Opaque namespace.
 
 Definition nroot : namespace := nil.
 
-Definition ndot_def `{Countable A} (N : namespace) (x : A) : namespace :=
+Local Definition ndot_def `{Countable A} (N : namespace) (x : A) : namespace :=
   encode x :: N.
-Definition ndot_aux : seal (@ndot_def). by eexists. Qed.
+Local Definition ndot_aux : seal (@ndot_def). by eexists. Qed.
 Definition ndot {A A_dec A_count}:= unseal ndot_aux A A_dec A_count.
-Definition ndot_eq : @ndot = @ndot_def := seal_eq ndot_aux.
+Local Definition ndot_unseal : @ndot = @ndot_def := seal_eq ndot_aux.
 
-Definition nclose_def (N : namespace) : coPset :=
+Local Definition nclose_def (N : namespace) : coPset :=
   coPset_suffixes (positives_flatten N).
-Definition nclose_aux : seal (@nclose_def). by eexists. Qed.
+Local Definition nclose_aux : seal (@nclose_def). by eexists. Qed.
 Global Instance nclose : UpClose namespace coPset := unseal nclose_aux.
-Definition nclose_eq : @nclose = @nclose_def := seal_eq nclose_aux.
+Local Definition nclose_unseal : @nclose = @nclose_def := seal_eq nclose_aux.
 
 Notation "N .@ x" := (ndot N x)
   (at level 19, left associativity, format "N .@ x") : stdpp_scope.
@@ -33,14 +33,14 @@ Section namespace.
   Implicit Types E : coPset.
 
   Global Instance ndot_inj : Inj2 (=) (=) (=) (@ndot A _ _).
-  Proof. intros N1 x1 N2 x2; rewrite !ndot_eq; naive_solver. Qed.
+  Proof. intros N1 x1 N2 x2; rewrite !ndot_unseal; naive_solver. Qed.
 
   Lemma nclose_nroot : ↑nroot = (⊤:coPset).
-  Proof. rewrite nclose_eq. by apply (sig_eq_pi _). Qed.
+  Proof. rewrite nclose_unseal. by apply (sig_eq_pi _). Qed.
 
   Lemma nclose_subseteq N x : ↑N.@x ⊆ (↑N : coPset).
   Proof.
-    intros p. unfold up_close. rewrite !nclose_eq, !ndot_eq.
+    intros p. unfold up_close. rewrite !nclose_unseal, !ndot_unseal.
     unfold nclose_def, ndot_def; rewrite !elem_coPset_suffixes.
     intros [q ->]. destruct (positives_flatten_suffix N (ndot_def N x)) as [q' ?].
     { by exists [encode x]. }
@@ -51,11 +51,11 @@ Section namespace.
   Proof. intros. etrans; eauto using nclose_subseteq. Qed.
 
   Lemma nclose_infinite N : ¬set_finite (↑ N : coPset).
-  Proof. rewrite nclose_eq. apply coPset_suffixes_infinite. Qed.
+  Proof. rewrite nclose_unseal. apply coPset_suffixes_infinite. Qed.
 
   Lemma ndot_ne_disjoint N x y : x ≠ y → N.@x ## N.@y.
   Proof.
-    intros Hxy a. unfold up_close. rewrite !nclose_eq, !ndot_eq.
+    intros Hxy a. unfold up_close. rewrite !nclose_unseal, !ndot_unseal.
     unfold nclose_def, ndot_def; rewrite !elem_coPset_suffixes.
     intros [qx ->] [qy Hqy].
     revert Hqy. by intros [= ?%(inj encode)]%positives_flatten_suffix_eq.