diff --git a/iris/base_logic/lib/gen_inv_heap.v b/iris/base_logic/lib/gen_inv_heap.v
index 62ca461369d7665e602578515857e4cd71edbde7..9ebda575a8e6bc2d6b769060c9b020d1da63e156 100644
--- a/iris/base_logic/lib/gen_inv_heap.v
+++ b/iris/base_logic/lib/gen_inv_heap.v
@@ -30,17 +30,17 @@ Definition to_inv_heap {L V : Type} `{Countable L}
     (h: gmap L (V * (V -d> PropO))) : inv_heap_mapUR L V :=
   prod_map (λ x, Excl' x) to_agree <$> h.
 
+Class inv_heapPreG (L V : Type) (Σ : gFunctors) `{Countable L} := {
+  inv_heap_preG_inG :> inG Σ (authR (inv_heap_mapUR L V))
+}.
+
 Class inv_heapG (L V : Type) (Σ : gFunctors) `{Countable L} := Inv_HeapG {
-  inv_heap_inG :> inG Σ (authR (inv_heap_mapUR L V));
+  inv_heap_inG :> inv_heapPreG L V Σ;
   inv_heap_name : gname
 }.
 Global Arguments Inv_HeapG _ _ {_ _ _ _}.
 Global Arguments inv_heap_name {_ _ _ _ _} _ : assert.
 
-Class inv_heapPreG (L V : Type) (Σ : gFunctors) `{Countable L} := {
-  inv_heap_preG_inG :> inG Σ (authR (inv_heap_mapUR L V))
-}.
-
 Definition inv_heapΣ (L V : Type) `{Countable L} : gFunctors :=
   #[ GFunctor (authR (inv_heap_mapUR L V)) ].
 
diff --git a/iris/base_logic/lib/proph_map.v b/iris/base_logic/lib/proph_map.v
index f28cce42516ce698570f5c8e5641864be89b0f08..fbed2c8b515b2a9ef91d1a00d67e2af7fb6fee7e 100644
--- a/iris/base_logic/lib/proph_map.v
+++ b/iris/base_logic/lib/proph_map.v
@@ -8,15 +8,16 @@ Local Notation proph_map P V := (gmap P (list V)).
 Definition proph_val_list (P V : Type) := list (P * V).
 
 (** The CMRA we need. *)
+Class proph_mapPreG (P V : Type) (Σ : gFunctors) `{Countable P} := {
+  proph_map_preG_inG :> inG Σ (gmap_viewR P (listO $ leibnizO V))
+}.
+
 Class proph_mapG (P V : Type) (Σ : gFunctors) `{Countable P} := ProphMapG {
-  proph_map_inG :> inG Σ (gmap_viewR P (listO $ leibnizO V));
+  proph_map_inG :> proph_mapPreG P V Σ;
   proph_map_name : gname
 }.
 Global Arguments proph_map_name {_ _ _ _ _} _ : assert.
 
-Class proph_mapPreG (P V : Type) (Σ : gFunctors) `{Countable P} :=
-  { proph_map_preG_inG :> inG Σ (gmap_viewR P (listO $ leibnizO V)) }.
-
 Definition proph_mapΣ (P V : Type) `{Countable P} : gFunctors :=
   #[GFunctor (gmap_viewR P (listO $ leibnizO V))].
 
diff --git a/iris/base_logic/lib/wsat.v b/iris/base_logic/lib/wsat.v
index 5092971c73725f2f21a4058a1356ea9e018baa33..37ddb62df1b634f4524cabf1e10914a45409aae3 100644
--- a/iris/base_logic/lib/wsat.v
+++ b/iris/base_logic/lib/wsat.v
@@ -8,10 +8,14 @@ From iris.prelude Require Import options.
 exception of what's in the [invG] module. The module [invG] is thus exported in
 [fancy_updates], which [wsat] is only imported. *)
 Module invG.
-  Class invG (Σ : gFunctors) : Set := WsatG {
-    inv_inG :> inG Σ (gmap_viewR positive (laterO (iPropO Σ)));
-    enabled_inG :> inG Σ coPset_disjR;
-    disabled_inG :> inG Σ (gset_disjR positive);
+  Class invPreG (Σ : gFunctors) : Set := InvPreG {
+    inv_inPreG :> inG Σ (gmap_viewR positive (laterO (iPropO Σ)));
+    enabled_inPreG :> inG Σ coPset_disjR;
+    disabled_inPreG :> inG Σ (gset_disjR positive);
+  }.
+
+  Class invG (Σ : gFunctors) : Set := InvG {
+    inv_inG :> invPreG Σ;
     invariant_name : gname;
     enabled_name : gname;
     disabled_name : gname;
@@ -22,12 +26,6 @@ Module invG.
       GFunctor coPset_disjR;
       GFunctor (gset_disjR positive)].
 
-  Class invPreG (Σ : gFunctors) : Set := WsatPreG {
-    inv_inPreG :> inG Σ (gmap_viewR positive (laterO (iPropO Σ)));
-    enabled_inPreG :> inG Σ coPset_disjR;
-    disabled_inPreG :> inG Σ (gset_disjR positive);
-  }.
-
   Global Instance subG_invΣ {Σ} : subG invΣ Σ → invPreG Σ.
   Proof. solve_inG. Qed.
 End invG.
@@ -192,7 +190,7 @@ Proof.
     first by apply gmap_view_auth_valid.
   iMod (own_alloc (CoPset ⊤)) as (γE) "HE"; first done.
   iMod (own_alloc (GSet ∅)) as (γD) "HD"; first done.
-  iModIntro; iExists (WsatG _ _ _ _ γI γE γD).
+  iModIntro; iExists (InvG _ _ γI γE γD).
   rewrite /wsat /ownE -lock; iFrame.
   iExists ∅. rewrite fmap_empty big_opM_empty. by iFrame.
 Qed.