diff --git a/program_logic/namespaces.v b/program_logic/namespaces.v
index 02e2a8dd6ec13c99ecde21d499b38c258b7fa19c..5badaaded9f02f7c05dec7d870b63a6f430e1a61 100644
--- a/program_logic/namespaces.v
+++ b/program_logic/namespaces.v
@@ -2,6 +2,10 @@ From iris.prelude Require Export countable coPset.
 From iris.algebra Require Export base.
 
 Definition namespace := list positive.
+Instance namespace_dec (N1 N2 : namespace) : Decision (N1 = N2) := _.
+Instance namespace_countable : Countable namespace := _.
+Typeclasses Opaque namespace.
+
 Definition nroot : namespace := nil.
 
 Definition ndot_def `{Countable A} (N : namespace) (x : A) : namespace :=