Renaming again [na_inG] and adding [na_invΣ] and [subG_na_invG].

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 Σ}.