diff --git a/iris/base_logic/lib/na_invariants.v b/iris/base_logic/lib/na_invariants.v
index d59861a8926fbc809b326e3a22eb23dfa30ad380..1f32d113451280ee092e0866661fd695921ecb88 100644
--- a/iris/base_logic/lib/na_invariants.v
+++ b/iris/base_logic/lib/na_invariants.v
@@ -23,7 +23,7 @@ Section defs.
 
   Definition na_inv (p : na_inv_pool_name) (N : namespace) (P : iProp Σ) : iProp Σ :=
     ∃ i, ⌜i ∈ (↑N:coPset)⌝ ∧
-         inv N (P ∗ own p (CoPset ∅, GSet {[i]}) ∨ na_own p {[i]}).
+         inv N (P ∗ own p (ε, GSet {[i]}) ∨ na_own p {[i]}).
 End defs.
 
 Global Instance: Params (@na_inv) 3 := {}.