diff --git a/theories/base_logic/lib/cancelable_invariants.v b/theories/base_logic/lib/cancelable_invariants.v
index 451fb5b0e464ed5063b803fdffe93b032335cf3d..b2bbd5cba9d897463a5057f4fa343f62ea2791f1 100644
--- a/theories/base_logic/lib/cancelable_invariants.v
+++ b/theories/base_logic/lib/cancelable_invariants.v
@@ -5,6 +5,10 @@ Set Default Proof Using "Type".
 Import uPred.
 
 Class cinvG Σ := cinv_inG :> inG Σ fracR.
+Definition cinvΣ : gFunctors := #[GFunctor fracR].
+
+Instance subG_cinvΣ {Σ} : subG cinvΣ Σ → cinvG Σ.
+Proof. solve_inG. Qed.
 
 Section defs.
   Context `{invG Σ, cinvG Σ}.