diff --git a/theories/base_logic/lib/na_invariants.v b/theories/base_logic/lib/na_invariants.v
index 68c7935bc920afd3232e61544ac3ede4a4cd9a60..6f760c91e99054dcd13a67d8977c69959a4526b2 100644
--- a/theories/base_logic/lib/na_invariants.v
+++ b/theories/base_logic/lib/na_invariants.v
@@ -9,7 +9,11 @@ Import uPred.
 Definition na_inv_pool_name := gname.
 
 Class na_invG Σ :=
-  na_inG :> inG Σ (prodR coPset_disjR (gset_disjR positive)).
+  na_inv_inG :> inG Σ (prodR coPset_disjR (gset_disjR positive)).
+Definition na_invΣ : gFunctors :=
+  #[ GFunctor (constRF (prodR coPset_disjR (gset_disjR positive))) ].
+Instance subG_na_invG {Σ} : subG na_invΣ Σ → na_invG Σ.
+Proof. solve_inG. Qed.
 
 Section defs.
   Context `{invG Σ, na_invG Σ}.