diff --git a/theories/lang/adequacy.v b/theories/lang/adequacy.v
index e86deef4d28360e82e70907a490ba3eba17fdd57..8ce55710e5653aeff598b63aa56417b9910c5e4d 100644
--- a/theories/lang/adequacy.v
+++ b/theories/lang/adequacy.v
@@ -4,21 +4,21 @@ From lrust.lang Require Export heap.
 From lrust.lang Require Import proofmode notation.
 Set Default Proof Using "Type".
 
-Class lrustPreG Σ := HeapGpreS {
-  lrust_preG_irig :> invGpreS Σ;
-  lrust_preG_heap :> inG Σ (authR heapUR);
-  lrust_preG_heap_freeable :> inG Σ (authR heap_freeableUR)
+Class lrustGpreS Σ := HeapGpreS {
+  lrustGpreS_irig :> invGpreS Σ;
+  lrustGpreS_heap :> inG Σ (authR heapUR);
+  lrustGpreS_heap_freeable :> inG Σ (authR heap_freeableUR)
 }.
 
 Definition lrustΣ : gFunctors :=
   #[invΣ;
     GFunctor (constRF (authR heapUR));
     GFunctor (constRF (authR heap_freeableUR))].
-Instance subG_heapPreG {Σ} : subG lrustΣ Σ → lrustPreG Σ.
+Instance subG_lrustGpreS {Σ} : subG lrustΣ Σ → lrustGpreS Σ.
 Proof. solve_inG. Qed.
 
-Definition lrust_adequacy Σ `{!lrustPreG Σ} e σ φ :
-  (∀ `{!lrustG Σ}, True ⊢ WP e {{ v, ⌜φ v⌝ }}) →
+Definition lrust_adequacy Σ `{!lrustGpreS Σ} e σ φ :
+  (∀ `{!lrustGS Σ}, True ⊢ WP e {{ v, ⌜φ v⌝ }}) →
   adequate NotStuck e σ (λ v _, φ v).
 Proof.
   intros Hwp; eapply (wp_adequacy _ _); iIntros (??).
@@ -29,5 +29,5 @@ Proof.
   set (Hheap := HeapGS _ _ _ vγ fγ).
   iModIntro. iExists (λ σ _, heap_ctx σ), (λ _, True%I). iSplitL.
   { iExists ∅. by iFrame. }
-  by iApply (Hwp (LRustG _ _ Hheap)).
+  by iApply (Hwp (LRustGS _ _ Hheap)).
 Qed.
diff --git a/theories/lang/lib/arc.v b/theories/lang/lib/arc.v
index 06f2a7af62f73d19341b6089c1684637296d90cb..528ea5c1d1062497329021d7c0635a59b44ddea8 100644
--- a/theories/lang/lib/arc.v
+++ b/theories/lang/lib/arc.v
@@ -114,7 +114,7 @@ Instance subG_arcΣ {Σ} : subG arcΣ Σ → arcG Σ.
 Proof. solve_inG. Qed.
 
 Section def.
-  Context `{!lrustG Σ, !arcG Σ} (P1 : Qp → iProp Σ) (P2 : iProp Σ) (N : namespace).
+  Context `{!lrustGS Σ, !arcG Σ} (P1 : Qp → iProp Σ) (P2 : iProp Σ) (N : namespace).
 
   Definition arc_tok γ q : iProp Σ :=
     own γ (◯ (Some $ Cinl (q, 1%positive, None), 0%nat)).
@@ -158,7 +158,7 @@ Section arc.
      this is the lifetime token), and P2 is the thing that is owned by the
      protocol when only weak references are left (in practice, P2 is the
      ownership of the underlying memory incl. deallocation). *)
-  Context `{!lrustG Σ, !arcG Σ} (P1 : Qp → iProp Σ) {HP1:Fractional P1}
+  Context `{!lrustGS Σ, !arcG Σ} (P1 : Qp → iProp Σ) {HP1:Fractional P1}
           (P2 : iProp Σ) (N : namespace).
 
   Instance P1_AsFractional q : AsFractional (P1 q) P1 q.
diff --git a/theories/lang/lib/lock.v b/theories/lang/lib/lock.v
index ae421b61f2e38d2f8cdd8197bf612fe30761e864..364aba416eef07415e5ce51a71b1d3352260fe29 100644
--- a/theories/lang/lib/lock.v
+++ b/theories/lang/lib/lock.v
@@ -16,7 +16,7 @@ Definition release : val := λ: ["l"], "l" <-ˢᶜ #false.
    their cancelling view shift has a non-empty mask, and it would have to be
    executed in the consequence view shift of a borrow. *)
 Section proof.
-  Context `{!lrustG Σ}.
+  Context `{!lrustGS Σ}.
 
   Definition lock_proto (l : loc) (R : iProp Σ) : iProp Σ :=
     (∃ b : bool, l ↦ #b ∗ if b then True else R)%I.
diff --git a/theories/lang/lib/memcpy.v b/theories/lang/lib/memcpy.v
index 1897f020e25751f64a39df1e73e65da12b039285..3b70cb9066453e5581fa09436a6b0d4e7fdd09e9 100644
--- a/theories/lang/lib/memcpy.v
+++ b/theories/lang/lib/memcpy.v
@@ -19,7 +19,7 @@ Notation "e1 <-{ n ',Σ' i } ! e2" :=
   (at level 80, n, i at next level,
    format "e1  <-{ n ,Σ  i }  ! e2") : expr_scope.
 
-Lemma wp_memcpy `{!lrustG Σ} E l1 l2 vl1 vl2 q (n : Z):
+Lemma wp_memcpy `{!lrustGS Σ} E l1 l2 vl1 vl2 q (n : Z):
   Z.of_nat (length vl1) = n → Z.of_nat (length vl2) = n →
   {{{ l1 ↦∗ vl1 ∗ l2 ↦∗{q} vl2 }}}
     #l1 <-{n} !#l2 @ E
diff --git a/theories/lang/lib/new_delete.v b/theories/lang/lib/new_delete.v
index 6a4be069df2e8d00a919f3c3f73d943e936ed092..3e049e4463d6ec317bd24c3093d77b1c28baaf9a 100644
--- a/theories/lang/lib/new_delete.v
+++ b/theories/lang/lib/new_delete.v
@@ -13,7 +13,7 @@ Definition delete : val :=
     else Free "n" "loc".
 
 Section specs.
-  Context `{!lrustG Σ}.
+  Context `{!lrustGS Σ}.
 
   Lemma wp_new E n:
     0 ≤ n →
diff --git a/theories/lang/lib/spawn.v b/theories/lang/lib/spawn.v
index 55feed47684cd7ab003735cea52441fc0f52bae2..c603babc0e1e536d7768f5f7a1dc606e607a5aca 100644
--- a/theories/lang/lib/spawn.v
+++ b/theories/lang/lib/spawn.v
@@ -36,7 +36,7 @@ Proof. solve_inG. Qed.
 
 (** Now we come to the Iris part of the proof. *)
 Section proof.
-Context `{!lrustG Σ, !spawnG Σ} (N : namespace).
+Context `{!lrustGS Σ, !spawnG Σ} (N : namespace).
 
 Definition spawn_inv (γf γj : gname) (c : loc) (Ψ : val → iProp Σ) : iProp Σ :=
   (own γf (Excl ()) ∗ own γj (Excl ()) ∨
diff --git a/theories/lang/lib/swap.v b/theories/lang/lib/swap.v
index d182c900cf72ad3248326c888b4343540b8c047b..e6997bbe414128c467d5869ef3ac08783f4c7421 100644
--- a/theories/lang/lib/swap.v
+++ b/theories/lang/lib/swap.v
@@ -10,7 +10,7 @@ Definition swap : val :=
          "p2" <- "x";;
          "swap" ["p1" +â‚— #1 ; "p2" +â‚— #1 ; "len" - #1].
 
-Lemma wp_swap `{!lrustG Σ} E l1 l2 vl1 vl2 (n : Z):
+Lemma wp_swap `{!lrustGS Σ} E l1 l2 vl1 vl2 (n : Z):
   Z.of_nat (length vl1) = n → Z.of_nat (length vl2) = n →
   {{{ l1 ↦∗ vl1 ∗ l2 ↦∗ vl2 }}}
     swap [ #l1; #l2; #n] @ E
diff --git a/theories/lang/lib/tests.v b/theories/lang/lib/tests.v
index 8f414deb52aa61ec33e4e20b76385cd83febbc64..82b76da0b124113df8fad871355698db48fafc39 100644
--- a/theories/lang/lib/tests.v
+++ b/theories/lang/lib/tests.v
@@ -4,7 +4,7 @@ From lrust.lang Require Import lang proofmode notation.
 Set Default Proof Using "Type".
 
 Section tests.
-  Context `{!lrustG Σ}.
+  Context `{!lrustGS Σ}.
 
   Lemma test_location_cmp E (l1 l2 : loc) q1 q2 v1 v2 :
     {{{ ▷ l1 ↦{q1} v1 ∗ ▷ l2 ↦{q2} v2 }}}
diff --git a/theories/lang/lifting.v b/theories/lang/lifting.v
index 9f869980a4b3e1e3e118e005ea3b9613fd6ccf8d..38567f42bd18b6d71a39355e308b7c114c0274c2 100644
--- a/theories/lang/lifting.v
+++ b/theories/lang/lifting.v
@@ -6,13 +6,13 @@ From lrust.lang Require Import tactics.
 Set Default Proof Using "Type".
 Import uPred.
 
-Class lrustG Σ := LRustG {
-  lrustG_invG : invGS Σ;
-  lrustG_gen_heapG :> heapGS Σ
+Class lrustGS Σ := LRustGS {
+  lrustGS_invGS : invGS Σ;
+  lrustGS_heapGS :> heapGS Σ
 }.
 
-Instance lrustG_irisG `{!lrustG Σ} : irisGS lrust_lang Σ := {
-  iris_invG := lrustG_invG;
+Instance lrustGS_irisGS `{!lrustGS Σ} : irisGS lrust_lang Σ := {
+  iris_invG := lrustGS_invGS;
   state_interp σ _ κs _ := heap_ctx σ;
   fork_post _ := True%I;
   num_laters_per_step _ := 0%nat;
@@ -63,7 +63,7 @@ Instance do_subst_vec xl (vsl : vec val (length xl)) e :
 Proof. by rewrite /DoSubstL subst_v_eq. Qed.
 
 Section lifting.
-Context `{!lrustG Σ}.
+Context `{!lrustGS Σ}.
 Implicit Types P Q : iProp Σ.
 Implicit Types e : expr.
 Implicit Types ef : option expr.
diff --git a/theories/lang/proofmode.v b/theories/lang/proofmode.v
index ef5c8bd70b9cefd5f0f86c94a7dec39ecbc795c2..3ea0ab9ffe59f7a13e8db77f598a887add0a8687 100644
--- a/theories/lang/proofmode.v
+++ b/theories/lang/proofmode.v
@@ -6,14 +6,14 @@ From lrust.lang Require Export tactics lifting.
 Set Default Proof Using "Type".
 Import uPred.
 
-Lemma tac_wp_value `{!lrustG Σ} Δ E Φ e v :
+Lemma tac_wp_value `{!lrustGS Σ} Δ E Φ e v :
   IntoVal e v →
   envs_entails Δ (Φ v) → envs_entails Δ (WP e @ E {{ Φ }}).
 Proof. rewrite envs_entails_eq=> ? ->. by apply wp_value. Qed.
 
 Ltac wp_value_head := eapply tac_wp_value; [iSolveTC|reduction.pm_prettify].
 
-Lemma tac_wp_pure `{!lrustG Σ} K Δ Δ' E e1 e2 φ n Φ :
+Lemma tac_wp_pure `{!lrustGS Σ} K Δ Δ' E e1 e2 φ n Φ :
   PureExec φ n e1 e2 →
   φ →
   MaybeIntoLaterNEnvs n Δ Δ' →
@@ -38,7 +38,7 @@ Tactic Notation "wp_pure" open_constr(efoc) :=
   | _ => fail "wp_pure: not a 'wp'"
   end.
 
-Lemma tac_wp_eq_loc `{!lrustG Σ} K Δ Δ' E i1 i2 l1 l2 q1 q2 v1 v2 Φ :
+Lemma tac_wp_eq_loc `{!lrustGS Σ} K Δ Δ' E i1 i2 l1 l2 q1 q2 v1 v2 Φ :
   MaybeIntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i1 Δ' = Some (false, l1 ↦{q1} v1)%I →
   envs_lookup i2 Δ' = Some (false, l2 ↦{q2} v2)%I →
@@ -67,7 +67,7 @@ Tactic Notation "wp_op" := wp_pure (BinOp _ _ _) || wp_eq_loc.
 Tactic Notation "wp_if" := wp_pure (If _ _ _).
 Tactic Notation "wp_case" := wp_pure (Case _ _); try wp_value_head.
 
-Lemma tac_wp_bind `{!lrustG Σ} K Δ E Φ e :
+Lemma tac_wp_bind `{!lrustGS Σ} K Δ E Φ e :
   envs_entails Δ (WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }})%I →
   envs_entails Δ (WP fill K e @ E {{ Φ }}).
 Proof. rewrite envs_entails_eq=> ->. apply: wp_bind. Qed.
@@ -89,7 +89,7 @@ Tactic Notation "wp_bind" open_constr(efoc) :=
   end.
 
 Section heap.
-Context `{!lrustG Σ}.
+Context `{!lrustGS Σ}.
 Implicit Types P Q : iProp Σ.
 Implicit Types Φ : val → iProp Σ.
 Implicit Types Δ : envs (uPredI (iResUR Σ)).
diff --git a/theories/lifetime/at_borrow.v b/theories/lifetime/at_borrow.v
index 04bd55a8b4adcb8932ffb95088143ce12ea78c4c..84d0c0522919de659ac0242f734fcabe7aa86ac6 100644
--- a/theories/lifetime/at_borrow.v
+++ b/theories/lifetime/at_borrow.v
@@ -5,14 +5,14 @@ Set Default Proof Using "Type".
 
 (** Atomic persistent bors  *)
 (* TODO : update the TEX with the fact that we can choose the namespace. *)
-Definition at_bor `{!invGS Σ, !lftG Σ userE} κ N (P : iProp Σ) :=
+Definition at_bor `{!invGS Σ, !lftGS Σ userE} κ N (P : iProp Σ) :=
   (∃ i, &{κ,i}P ∗
     (⌜N ## lftN⌝ ∗ inv N (idx_bor_own 1 i) ∨
      ⌜N = lftN⌝ ∗ inv N (∃ q, idx_bor_own q i)))%I.
 Notation "&at{ κ , N }" := (at_bor κ N) (format "&at{ κ , N }") : bi_scope.
 
 Section atomic_bors.
-  Context `{!invGS Σ, !lftG Σ userE} (P : iProp Σ) (N : namespace).
+  Context `{!invGS Σ, !lftGS Σ userE} (P : iProp Σ) (N : namespace).
 
   Global Instance at_bor_ne κ n : Proper (dist n ==> dist n) (at_bor κ N).
   Proof. solve_proper. Qed.
@@ -97,7 +97,7 @@ Section atomic_bors.
   Qed.
 End atomic_bors.
 
-Lemma at_bor_acc_lftN `{!invGS Σ, !lftG Σ userE} (P : iProp Σ) E κ :
+Lemma at_bor_acc_lftN `{!invGS Σ, !lftGS Σ userE} (P : iProp Σ) E κ :
   ↑lftN ⊆ E →
   lft_ctx -∗ &at{κ,lftN}P ={E,E∖↑lftN}=∗ ▷P ∗ (▷P ={E∖↑lftN,E}=∗ True) ∨
              [†κ] ∗ |={E∖↑lftN,E}=> True.
diff --git a/theories/lifetime/frac_borrow.v b/theories/lifetime/frac_borrow.v
index 2874a6609c1d3ac135788361f3bed26b797f3bb6..6c88d97e2c921b0ed8e6aa484e4c207d7f1ad646 100644
--- a/theories/lifetime/frac_borrow.v
+++ b/theories/lifetime/frac_borrow.v
@@ -6,16 +6,16 @@ Set Default Proof Using "Type".
 
 Class frac_borG Σ := frac_borG_inG :> inG Σ fracR.
 
-Local Definition frac_bor_inv `{!invGS Σ, !lftG Σ userE, !frac_borG Σ}
+Local Definition frac_bor_inv `{!invGS Σ, !lftGS Σ userE, !frac_borG Σ}
                               (φ : Qp → iProp Σ) γ κ' :=
   (∃ q, φ q ∗ own γ q ∗ (⌜q = 1%Qp⌝ ∨ ∃ q', ⌜(q + q' = 1)%Qp⌝ ∗ q'.[κ']))%I.
 
-Definition frac_bor `{!invGS Σ, !lftG Σ userE, !frac_borG Σ} κ (φ : Qp → iProp Σ) :=
+Definition frac_bor `{!invGS Σ, !lftGS Σ userE, !frac_borG Σ} κ (φ : Qp → iProp Σ) :=
   (∃ γ κ', κ ⊑ κ' ∗ &at{κ',lftN} (frac_bor_inv φ γ κ'))%I.
 Notation "&frac{ κ }" := (frac_bor κ) (format "&frac{ κ }") : bi_scope.
 
 Section frac_bor.
-  Context `{!invGS Σ, !lftG Σ userE, !frac_borG Σ} (φ : Qp → iProp Σ).
+  Context `{!invGS Σ, !lftGS Σ userE, !frac_borG Σ} (φ : Qp → iProp Σ).
   Implicit Types E : coPset.
 
   Global Instance frac_bor_contractive κ n :
@@ -155,7 +155,7 @@ Section frac_bor.
   Qed.
 End frac_bor.
 
-Lemma frac_bor_lft_incl `{!invGS Σ, !lftG Σ userE, !frac_borG Σ} κ κ' q:
+Lemma frac_bor_lft_incl `{!invGS Σ, !lftGS Σ userE, !frac_borG Σ} κ κ' q:
   lft_ctx -∗ &frac{κ}(λ q', (q * q').[κ']) -∗ κ ⊑ κ'.
 Proof.
   iIntros "#LFT#Hbor". iApply lft_incl_intro. iModIntro. iSplitR.
diff --git a/theories/lifetime/lifetime.v b/theories/lifetime/lifetime.v
index 098a789eea16d18f5aade328f1aee49487ef04a7..1a8a9b3a2e6e1eb0fb71ac868c404f965f788d5b 100644
--- a/theories/lifetime/lifetime.v
+++ b/theories/lifetime/lifetime.v
@@ -26,7 +26,7 @@ Definition lft_incl_syntactic (κ κ' : lft) : Prop := ∃ κ'', κ'' ⊓ κ' =
 Infix "⊑ˢʸⁿ" := lft_incl_syntactic (at level 40) : stdpp_scope.
 
 Section derived.
-Context `{!invGS Σ, !lftG Σ userE}.
+Context `{!invGS Σ, !lftGS Σ userE}.
 Implicit Types κ : lft.
 
 Lemma lft_create E :
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index 84ed70d6a7e44a5bacd559d0d0b2992bd6be371d..345b819a235a3823fec2933e58c42ba5ec10396c 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -13,29 +13,29 @@ Module Type lifetime_sig.
      have aliases here. *)
   (** userE is a (disjoint) mask that is available in the "consequence" view
       shift of borrow accessors. *)
-  Parameter lftG' : ∀ (Σ : gFunctors) (userE : coPset), Set.
-  Global Notation lftG := lftG'.
-  Existing Class lftG'.
-  Parameter lftPreG' : gFunctors → Set.
-  Global Notation lftPreG := lftPreG'.
-  Existing Class lftPreG'.
+  Parameter lftGS' : ∀ (Σ : gFunctors) (userE : coPset), Set.
+  Global Notation lftGS := lftGS'.
+  Existing Class lftGS'.
+  Parameter lftGpreS' : gFunctors → Set.
+  Global Notation lftGpreS := lftGpreS'.
+  Existing Class lftGpreS'.
 
   (** * Definitions *)
   Parameter lft : Type.
   Parameter static : lft.
   Declare Instance lft_intersect : Meet lft.
 
-  Parameter lft_ctx : ∀ `{!invGS Σ, !lftG Σ userE}, iProp Σ.
+  Parameter lft_ctx : ∀ `{!invGS Σ, !lftGS Σ userE}, iProp Σ.
 
-  Parameter lft_tok : ∀ `{!lftG Σ userE} (q : Qp) (κ : lft), iProp Σ.
-  Parameter lft_dead : ∀ `{!lftG Σ userE} (κ : lft), iProp Σ.
+  Parameter lft_tok : ∀ `{!lftGS Σ userE} (q : Qp) (κ : lft), iProp Σ.
+  Parameter lft_dead : ∀ `{!lftGS Σ userE} (κ : lft), iProp Σ.
 
-  Parameter lft_incl : ∀ `{!invGS Σ, !lftG Σ userE} (κ κ' : lft), iProp Σ.
-  Parameter bor : ∀ `{!invGS Σ, !lftG Σ userE} (κ : lft) (P : iProp Σ), iProp Σ.
+  Parameter lft_incl : ∀ `{!invGS Σ, !lftGS Σ userE} (κ κ' : lft), iProp Σ.
+  Parameter bor : ∀ `{!invGS Σ, !lftGS Σ userE} (κ : lft) (P : iProp Σ), iProp Σ.
 
   Parameter bor_idx : Type.
-  Parameter idx_bor_own : ∀ `{!lftG Σ userE} (q : frac) (i : bor_idx), iProp Σ.
-  Parameter idx_bor : ∀ `{!invGS Σ, !lftG Σ userE} (κ : lft) (i : bor_idx) (P : iProp Σ), iProp Σ.
+  Parameter idx_bor_own : ∀ `{!lftGS Σ userE} (q : frac) (i : bor_idx), iProp Σ.
+  Parameter idx_bor : ∀ `{!invGS Σ, !lftGS Σ userE} (κ : lft) (i : bor_idx) (P : iProp Σ), iProp Σ.
 
   (** Our lifetime creation lemma offers allocating a lifetime that is defined
   by a [positive] in some given infinite set. This operation converts the
@@ -53,7 +53,7 @@ Module Type lifetime_sig.
   Infix "⊑" := lft_incl (at level 70) : bi_scope.
 
   Section properties.
-  Context `{!invGS Σ, !lftG Σ userE}.
+  Context `{!invGS Σ, !lftGS Σ userE}.
 
   (** * Instances *)
   Global Declare Instance lft_inhabited : Inhabited lft.
@@ -170,9 +170,9 @@ Module Type lifetime_sig.
   End properties.
 
   Parameter lftΣ : gFunctors.
-  Global Declare Instance subG_lftPreG Σ : subG lftΣ Σ → lftPreG Σ.
+  Global Declare Instance subG_lftGpreS Σ : subG lftΣ Σ → lftGpreS Σ.
 
-  Parameter lft_init : ∀ `{!invGS Σ, !lftPreG Σ} E userE,
+  Parameter lft_init : ∀ `{!invGS Σ, !lftGpreS Σ} E userE,
     ↑lftN ⊆ E → ↑lftN ## userE →
-    ⊢ |={E}=> ∃ _ : lftG Σ userE, lft_ctx.
+    ⊢ |={E}=> ∃ _ : lftGS Σ userE, lft_ctx.
 End lifetime_sig.
diff --git a/theories/lifetime/meta.v b/theories/lifetime/meta.v
index 62421fce0882a03907371c646ab72075010cc200..5872acd56e05188d8bb16032f86b94dc62ac0b3e 100644
--- a/theories/lifetime/meta.v
+++ b/theories/lifetime/meta.v
@@ -21,12 +21,12 @@ we need. In other words, we use [own_unit] instead of [own_alloc]. As a result
 we can just hard-code an arbitrary name here. *)
 Local Definition lft_meta_gname : gname := 42%positive.
 
-Definition lft_meta `{!lftG Σ userE, lft_metaG Σ} (κ : lft) (γ : gname) : iProp Σ :=
+Definition lft_meta `{!lftGS Σ userE, lft_metaG Σ} (κ : lft) (γ : gname) : iProp Σ :=
   ∃ p : positive, ⌜κ = positive_to_lft p⌝ ∗
     own lft_meta_gname (dyn_reservation_map_data p (to_agree γ)).
 
 Section lft_meta.
-  Context `{!invGS Σ, !lftG Σ userE, lft_metaG Σ}.
+  Context `{!invGS Σ, !lftGS Σ userE, lft_metaG Σ}.
 
   Global Instance lft_meta_timeless κ γ : Timeless (lft_meta κ γ).
   Proof. apply _. Qed.
diff --git a/theories/lifetime/model/accessors.v b/theories/lifetime/model/accessors.v
index bc460359549c54e5998f049ed61cd6905b834f65..58054f9ca77d730af155cc20e72b0dcad64ef015 100644
--- a/theories/lifetime/model/accessors.v
+++ b/theories/lifetime/model/accessors.v
@@ -5,7 +5,7 @@ From iris.base_logic.lib Require Import boxes.
 Set Default Proof Using "Type".
 
 Section accessors.
-Context `{!invGS Σ, !lftG Σ userE}.
+Context `{!invGS Σ, !lftGS Σ userE}.
 Implicit Types κ : lft.
 
 (* Helper internal lemmas *)
diff --git a/theories/lifetime/model/borrow.v b/theories/lifetime/model/borrow.v
index 982cc8d51dd03bbd7a37cea2ecc832c595bc7b71..aea3fa114016378ea5dc7e9d609da77b7064c137 100644
--- a/theories/lifetime/model/borrow.v
+++ b/theories/lifetime/model/borrow.v
@@ -6,7 +6,7 @@ From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 
 Section borrow.
-Context `{!invGS Σ, !lftG Σ userE}.
+Context `{!invGS Σ, !lftGS Σ userE}.
 Implicit Types κ : lft.
 
 Lemma raw_bor_create E κ P :
diff --git a/theories/lifetime/model/borrow_sep.v b/theories/lifetime/model/borrow_sep.v
index 9213e161a57308c4a801a402c2d31550b1759f7c..e01b8f518a517194562f3786323ae78f66823b56 100644
--- a/theories/lifetime/model/borrow_sep.v
+++ b/theories/lifetime/model/borrow_sep.v
@@ -6,7 +6,7 @@ From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 
 Section borrow.
-Context `{!invGS Σ, !lftG Σ userE}.
+Context `{!invGS Σ, !lftGS Σ userE}.
 Implicit Types κ : lft.
 
 Lemma bor_sep E κ P Q :
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index ac782d8fb49a94ee189900fa57650b94cd20b295..dbfdff98dff95b716b776af3e371a2e29d9caa15 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -6,7 +6,7 @@ From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 
 Section creation.
-Context `{!invGS Σ, !lftG Σ userE}.
+Context `{!invGS Σ, !lftGS Σ userE}.
 Implicit Types κ : lft.
 
 Lemma lft_kill (I : gmap lft lft_names) (K K' : gset lft) (κ : lft) :
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index 1a1f85e51bb8b7f791fe0beb20ddf4ac35acebea..2fc9c8bdd004b8ad318add426d8b142ed72da1c7 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -40,7 +40,7 @@ Definition ilftUR := gmapUR lft (agreeR lft_namesO).
 Definition borUR := gmapUR slice_name (prodR fracR (agreeR bor_stateO)).
 Definition inhUR := gset_disjUR slice_name.
 
-Class lftG Σ (userE : coPset) := LftG {
+Class lftGS Σ (userE : coPset) := LftG {
   lft_box :> boxG Σ;
   alft_inG :> inG Σ (authR alftUR);
   alft_name : gname;
@@ -51,9 +51,9 @@ Class lftG Σ (userE : coPset) := LftG {
   lft_inh_inG :> inG Σ (authR inhUR);
   userE_lftN_disj : ↑lftN ## userE;
 }.
-Definition lftG' := lftG.
+Definition lftGS' := lftGS.
 
-Class lftPreG Σ := LftPreG {
+Class lftGpreS Σ := LftGPreS {
   lft_preG_box :> boxG Σ;
   alft_preG_inG :> inG Σ (authR alftUR);
   ilft_preG_inG :> inG Σ (authR ilftUR);
@@ -61,13 +61,13 @@ Class lftPreG Σ := LftPreG {
   lft_preG_cnt_inG :> inG Σ (authR natUR);
   lft_preG_inh_inG :> inG Σ (authR inhUR);
 }.
-Definition lftPreG' := lftPreG.
+Definition lftGpreS' := lftGpreS.
 
 Definition lftΣ : gFunctors :=
   #[ boxΣ; GFunctor (authR alftUR); GFunctor (authR ilftUR);
      GFunctor (authR borUR); GFunctor (authR natUR); GFunctor (authR inhUR) ].
-Instance subG_lftPreG Σ :
-  subG lftΣ Σ → lftPreG Σ.
+Instance subG_lftGpreS Σ :
+  subG lftΣ Σ → lftGpreS Σ.
 Proof. solve_inG. Qed.
 
 Definition bor_filled (s : bor_state) : bool :=
@@ -80,7 +80,7 @@ Definition to_ilftUR : gmap lft lft_names → ilftUR := fmap to_agree.
 Definition to_borUR : gmap slice_name bor_state → borUR := fmap ((1%Qp,.) ∘ to_agree).
 
 Section defs.
-  Context `{!invGS Σ, !lftG Σ userE}.
+  Context `{!invGS Σ, !lftGS Σ userE}.
 
   Definition lft_tok (q : Qp) (κ : lft) : iProp Σ :=
     ([∗ mset] Λ ∈ κ, own alft_name (◯ {[ Λ := Cinl q ]}))%I.
@@ -224,7 +224,7 @@ Typeclasses Opaque lft_tok lft_dead bor_cnt lft_bor_alive lft_bor_dead
   idx_bor_own idx_bor raw_bor bor.
 
 Section basic_properties.
-Context `{!invGS Σ, !lftG Σ userE}.
+Context `{!invGS Σ, !lftGS Σ userE}.
 Implicit Types κ : lft.
 
 (* Unfolding lemmas *)
diff --git a/theories/lifetime/model/faking.v b/theories/lifetime/model/faking.v
index 1e996cd1b2cd7e7411899fdb2c51a83cbfd531c5..1500524e90b6687b7344de1fa65c5ba1215ec51b 100644
--- a/theories/lifetime/model/faking.v
+++ b/theories/lifetime/model/faking.v
@@ -5,7 +5,7 @@ From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 
 Section faking.
-Context `{!invGS Σ, !lftG Σ userE}.
+Context `{!invGS Σ, !lftGS Σ userE}.
 Implicit Types κ : lft.
 
 Lemma ilft_create A I κ :
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index eaaf4991e9c154966ecdcbfbb96178ce18f14649..798d8d0e94ed7c918be8dfeadd91f92f6cba8529 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -6,13 +6,13 @@ From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 Import uPred.
 
-Lemma lft_init `{!invGS Σ, !lftPreG Σ} E userE :
-  ↑lftN ⊆ E → ↑lftN ## userE → ⊢ |={E}=> ∃ _ : lftG Σ userE, lft_ctx.
+Lemma lft_init `{!invGS Σ, !lftGpreS Σ} E userE :
+  ↑lftN ⊆ E → ↑lftN ## userE → ⊢ |={E}=> ∃ _ : lftGS Σ userE, lft_ctx.
 Proof.
   iIntros (? HuserE). rewrite /lft_ctx.
   iMod (own_alloc (● ∅ : authR alftUR)) as (γa) "Ha"; first by apply auth_auth_valid.
   iMod (own_alloc (● ∅ : authR ilftUR)) as (γi) "Hi"; first by apply auth_auth_valid.
-  set (HlftG := LftG _ _ _ _ γa _ γi _ _ _ HuserE). iExists HlftG.
+  set (HlftGS := LftG _ _ _ _ γa _ γi _ _ _ HuserE). iExists HlftGS.
   iMod (inv_alloc _ _ lfts_inv with "[Ha Hi]") as "$"; last done.
   iModIntro. rewrite /lfts_inv /own_alft_auth /own_ilft_auth. iExists ∅, ∅.
   rewrite /to_alftUR /to_ilftUR !fmap_empty. iFrame.
@@ -20,7 +20,7 @@ Proof.
 Qed.
 
 Section primitive.
-Context `{!invGS Σ, !lftG Σ userE}.
+Context `{!invGS Σ, !lftGS Σ userE}.
 Implicit Types κ : lft.
 
 Lemma to_borUR_included (B : gmap slice_name bor_state) i s q :
diff --git a/theories/lifetime/model/reborrow.v b/theories/lifetime/model/reborrow.v
index a77e597add827bd730acd9aff26c9c478052044a..7b0bce8616ac4cec74ec8f7f5212b81d55938081 100644
--- a/theories/lifetime/model/reborrow.v
+++ b/theories/lifetime/model/reborrow.v
@@ -5,7 +5,7 @@ From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 
 Section reborrow.
-Context `{!invGS Σ, !lftG Σ userE}.
+Context `{!invGS Σ, !lftGS Σ userE}.
 Implicit Types κ : lft.
 
 (* Notice that taking lft_inv for both κ and κ' already implies
diff --git a/theories/lifetime/na_borrow.v b/theories/lifetime/na_borrow.v
index fec690bc433258691da17a500e93829a8685d17b..729cc5769fbbd8b0a182454966879e5bb80b16c1 100644
--- a/theories/lifetime/na_borrow.v
+++ b/theories/lifetime/na_borrow.v
@@ -3,7 +3,7 @@ From iris.base_logic.lib Require Export na_invariants.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 
-Definition na_bor `{!invGS Σ, !lftG Σ userE, !na_invG Σ}
+Definition na_bor `{!invGS Σ, !lftGS Σ userE, !na_invG Σ}
            (κ : lft) (tid : na_inv_pool_name) (N : namespace) (P : iProp Σ) :=
   (∃ i, &{κ,i}P ∗ na_inv tid N (idx_bor_own 1 i))%I.
 
@@ -11,7 +11,7 @@ Notation "&na{ κ , tid , N }" := (na_bor κ tid N)
     (format "&na{ κ , tid , N }") : bi_scope.
 
 Section na_bor.
-  Context `{!invGS Σ, !lftG Σ userE, !na_invG Σ}
+  Context `{!invGS Σ, !lftGS Σ userE, !na_invG Σ}
           (tid : na_inv_pool_name) (N : namespace) (P : iProp Σ).
 
   Global Instance na_bor_ne κ n : Proper (dist n ==> dist n) (na_bor κ tid N).
diff --git a/theories/typing/bool.v b/theories/typing/bool.v
index 19c04dd697637ef7dbdec89f960e176d9b8c4d24..6c1e4f83df9331980d98f059374b9d91c8f7cf3f 100644
--- a/theories/typing/bool.v
+++ b/theories/typing/bool.v
@@ -4,7 +4,7 @@ From lrust.typing Require Import programs.
 Set Default Proof Using "Type".
 
 Section bool.
-  Context `{!typeG Σ}.
+  Context `{!typeGS Σ}.
 
   Program Definition bool : type :=
     {| st_own tid vl :=
@@ -22,7 +22,7 @@ Section bool.
 End bool.
 
 Section typing.
-  Context `{!typeG Σ}.
+  Context `{!typeGS Σ}.
 
   Lemma type_bool_instr (b : Datatypes.bool) : typed_val #b bool.
   Proof.
diff --git a/theories/typing/borrow.v b/theories/typing/borrow.v
index baf447ff044341e108f67dafeaa720168818ca75..ad909c549e8ea04d0720504cdf0dad706f5f7614 100644
--- a/theories/typing/borrow.v
+++ b/theories/typing/borrow.v
@@ -9,7 +9,7 @@ Set Default Proof Using "Type".
   concurrently. *)
 
 Section borrow.
-  Context `{!typeG Σ}.
+  Context `{!typeGS Σ}.
 
   Lemma tctx_borrow E L p n ty κ :
     tctx_incl E L [p ◁ own_ptr n ty] [p ◁ &uniq{κ}ty; p ◁{κ} own_ptr n ty].
diff --git a/theories/typing/cont.v b/theories/typing/cont.v
index 2d7d99ace081b83c2c7215b879016991a5b7b903..1cca20812ebe4d7115550c9c0e7601894641b6c2 100644
--- a/theories/typing/cont.v
+++ b/theories/typing/cont.v
@@ -4,7 +4,7 @@ From lrust.typing Require Import programs.
 Set Default Proof Using "Type".
 
 Section typing.
-  Context `{!typeG Σ}.
+  Context `{!typeGS Σ}.
 
   (** Jumping to and defining a continuation. *)
   Lemma type_jump args argsv E L C T k T' :
diff --git a/theories/typing/cont_context.v b/theories/typing/cont_context.v
index b76fdf65bb167958b2508255624e90990ef56456..ff78d9dbf33ced8914c5ebf0206e3e7248416b8e 100644
--- a/theories/typing/cont_context.v
+++ b/theories/typing/cont_context.v
@@ -4,7 +4,7 @@ From lrust.typing Require Import type lft_contexts type_context.
 Set Default Proof Using "Type".
 
 Section cont_context_def.
-  Context `{!typeG Σ}.
+  Context `{!typeGS Σ}.
 
   Definition cont_postcondition : iProp Σ := True%I.
 
@@ -20,7 +20,7 @@ Notation "k ◁cont( L , T )" := (CCtx_iscont k L _ T)
   (at level 70, format "k  ◁cont( L ,  T )").
 
 Section cont_context.
-  Context `{!typeG Σ}.
+  Context `{!typeGS Σ}.
 
   Definition cctx_elt_interp (tid : thread_id) (qmax: Qp) (x : cctx_elt) : iProp Σ :=
     let '(k ◁cont(L, T)) := x in
diff --git a/theories/typing/examples/get_x.v b/theories/typing/examples/get_x.v
index 3da2f4acec9826138bf4babf07ab669c7f8140b0..95486f6e0a040ad68e5a9fb8854516e00281210c 100644
--- a/theories/typing/examples/get_x.v
+++ b/theories/typing/examples/get_x.v
@@ -3,7 +3,7 @@ From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
 Section get_x.
-  Context `{!typeG Σ}.
+  Context `{!typeGS Σ}.
 
   Definition get_x : val :=
     fn: ["p"] :=
diff --git a/theories/typing/examples/init_prod.v b/theories/typing/examples/init_prod.v
index 2da3607365d18fb53a6cff2113d52a3fe1ea4881..ee0bc5baad3bb79d6243290226cb38dc6e28e92d 100644
--- a/theories/typing/examples/init_prod.v
+++ b/theories/typing/examples/init_prod.v
@@ -3,7 +3,7 @@ From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
 Section init_prod.
-  Context `{!typeG Σ}.
+  Context `{!typeGS Σ}.
 
   Definition init_prod : val :=
     fn: ["x"; "y"] :=
diff --git a/theories/typing/examples/lazy_lft.v b/theories/typing/examples/lazy_lft.v
index ca5b804e20ce6be74571c94b92fe2457c8320cc9..b9bf73543a0f9585f388ee187bab2666f0e2246b 100644
--- a/theories/typing/examples/lazy_lft.v
+++ b/theories/typing/examples/lazy_lft.v
@@ -3,7 +3,7 @@ From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
 Section lazy_lft.
-  Context `{!typeG Σ}.
+  Context `{!typeGS Σ}.
 
   Definition lazy_lft : val :=
     fn: [] :=
diff --git a/theories/typing/examples/nonlexical.v b/theories/typing/examples/nonlexical.v
index 64ad88b12cc50784249a399a485fb00eba60fe8a..2718f2e8138fb29a573e2ee524b0c1b4a355416e 100644
--- a/theories/typing/examples/nonlexical.v
+++ b/theories/typing/examples/nonlexical.v
@@ -13,7 +13,7 @@ From lrust.typing Require Import typing lib.option.
 *)
 
 Section non_lexical.
-  Context `{!typeG Σ} (HashMap K V : type)
+  Context `{!typeGS Σ} (HashMap K V : type)
           `{!TyWf hashmap, !TyWf K, !TyWf V, !Copy K}
           (defaultv get_mut insert: val).
 
diff --git a/theories/typing/examples/rebor.v b/theories/typing/examples/rebor.v
index 1dbac6cee2d109e58e62716b4f7b5a5384f34956..4b5cda264cbb41f19334a5118cc20f8d3031943d 100644
--- a/theories/typing/examples/rebor.v
+++ b/theories/typing/examples/rebor.v
@@ -3,7 +3,7 @@ From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
 Section rebor.
-  Context `{!typeG Σ}.
+  Context `{!typeGS Σ}.
 
   Definition rebor : val :=
     fn: ["t1"; "t2"] :=
diff --git a/theories/typing/examples/unbox.v b/theories/typing/examples/unbox.v
index 843b715f00b33a1a8d3003833f19aa8eec09e018..b1a13d010d4614c49029672d1cbc3cfedbeacc35 100644
--- a/theories/typing/examples/unbox.v
+++ b/theories/typing/examples/unbox.v
@@ -3,7 +3,7 @@ From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
 Section unbox.
-  Context `{!typeG Σ}.
+  Context `{!typeGS Σ}.
 
   Definition unbox : val :=
     fn: ["b"] :=
diff --git a/theories/typing/fixpoint.v b/theories/typing/fixpoint.v
index cec43a3b11867698208592029c461837a4145ad8..b35258a6e53b1dac02b8e9b0c030a1d536a71b9c 100644
--- a/theories/typing/fixpoint.v
+++ b/theories/typing/fixpoint.v
@@ -4,7 +4,7 @@ Set Default Proof Using "Type".
 Import uPred.
 
 Section fixpoint_def.
-  Context `{!typeG Σ}.
+  Context `{!typeGS Σ}.
   Context (T : type → type) {HT: TypeContractive T}.
 
   Global Instance type_inhabited : Inhabited type := populate bool.
@@ -37,13 +37,13 @@ Section fixpoint_def.
     {| ty_lfts := lfts; ty_wf_E := wf_E |}.
 End fixpoint_def.
 
-Lemma type_fixpoint_ne `{!typeG Σ} (T1 T2 : type → type)
+Lemma type_fixpoint_ne `{!typeGS Σ} (T1 T2 : type → type)
     `{!TypeContractive T1, !TypeContractive T2} n :
   (∀ t, T1 t ≡{n}≡ T2 t) → type_fixpoint T1 ≡{n}≡ type_fixpoint T2.
 Proof. eapply fixpointK_ne; apply type_contractive_ne, _. Qed.
 
 Section fixpoint.
-  Context `{!typeG Σ}.
+  Context `{!typeGS Σ}.
   Context (T : type → type) {HT: TypeContractive T}.
 
   Global Instance fixpoint_copy :
@@ -98,7 +98,7 @@ Section fixpoint.
 End fixpoint.
 
 Section subtyping.
-  Context `{!typeG Σ} (E : elctx) (L : llctx).
+  Context `{!typeGS Σ} (E : elctx) (L : llctx).
 
   (* TODO : is there a way to declare these as a [Proper] instances ? *)
   Lemma fixpoint_mono T1 `{!TypeContractive T1} T2 `{!TypeContractive T2} :
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 4e9a4f4c3ad46fd9bf119969bb3dab3dbed4112a..9eed7c5ece088bc0335118e3a058505ee90da650 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -5,7 +5,7 @@ From lrust.typing Require Import own programs cont.
 Set Default Proof Using "Type".
 
 Section fn.
-  Context `{!typeG Σ} {A : Type} {n : nat}.
+  Context `{!typeGS Σ} {A : Type} {n : nat}.
 
   Record fn_params := FP { fp_E : lft → elctx; fp_tys : vec type n; fp_ty : type }.
 
@@ -142,7 +142,7 @@ Notation "'fn(' E ')' '→' R" :=
 Instance elctx_empty : Empty (lft → elctx) := λ ϝ, [].
 
 Section typing.
-  Context `{!typeG Σ}.
+  Context `{!typeGS Σ}.
 
   Lemma fn_subtype {A n} E0 L0 (fp fp' : A → fn_params n) :
     (∀ x ϝ, let EE := E0 ++ (fp' x).(fp_E) ϝ in
diff --git a/theories/typing/int.v b/theories/typing/int.v
index c710360d37d9248a0d11644f1705c50c628749b8..4ec16f6dcaa7a1130470444a4ed8866abd1aaeee 100644
--- a/theories/typing/int.v
+++ b/theories/typing/int.v
@@ -4,7 +4,7 @@ From lrust.typing Require Import bool programs.
 Set Default Proof Using "Type".
 
 Section int.
-  Context `{!typeG Σ}.
+  Context `{!typeGS Σ}.
 
   Program Definition int : type :=
     {| st_own tid vl :=
@@ -22,7 +22,7 @@ Section int.
 End int.
 
 Section typing.
-  Context `{!typeG Σ}.
+  Context `{!typeGS Σ}.
 
   Lemma type_int_instr (z : Z) : typed_val #z int.
   Proof.
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index f869d85e283db9811ee4cda5dcf8af5ce521dfb9..0dc89dcf2f792ffc81e6a454447232b979efc3bd 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -23,7 +23,7 @@ Notation llctx := (list llctx_elt).
 Notation "κ ⊑ₗ κl" := (@pair lft (list lft) κ κl) (at level 70).
 
 Section lft_contexts.
-  Context `{!invGS Σ, !lftG Σ lft_userE}.
+  Context `{!invGS Σ, !lftGS Σ lft_userE}.
   Implicit Type (κ : lft).
 
   (* External lifetime contexts. *)
@@ -415,7 +415,7 @@ Arguments lctx_lft_incl_incl_noend {_ _ _ _} _ _.
 Arguments lctx_lft_alive_tok {_ _ _ _ _} _ _ _.
 Arguments lctx_lft_alive_tok_noend {_ _ _ _ _} _ _ _.
 
-Lemma elctx_sat_submseteq `{!invGS Σ, !lftG Σ lft_userE} E E' L :
+Lemma elctx_sat_submseteq `{!invGS Σ, !lftGS Σ lft_userE} E E' L :
   E' ⊆+ E → elctx_sat E L E'.
 Proof. iIntros (HE' ??) "_ !> H". by iApply big_sepL_submseteq. Qed.
 
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index c85c868c70a8664e251b7e3822259b54564650bf..7eed83f49bdfdbf9b2c1ef151525bb56f2464da8 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -13,7 +13,7 @@ Definition arc_shrN := arcN .@ "shr".
 Definition arc_endN := arcN .@ "end".
 
 Section arc.
-  Context `{!typeG Σ, !arcG Σ}.
+  Context `{!typeGS Σ, !arcG Σ}.
 
   (* Preliminary definitions. *)
   Let P1 ν q := (q.[ν])%I.
diff --git a/theories/typing/lib/brandedvec.v b/theories/typing/lib/brandedvec.v
index 8a12af7611d96e067b836246ea9ea055bd4ba581..979b61d8ede92f7778eeff2febc67dd36ca4df73 100644
--- a/theories/typing/lib/brandedvec.v
+++ b/theories/typing/lib/brandedvec.v
@@ -21,7 +21,7 @@ Definition brandidxN := lrustN .@ "brandix".
 Definition brandvecN := lrustN .@ "brandvec".
 
 Section brandedvec.
-  Context `{!typeG Σ, !brandidxG Σ}.
+  Context `{!typeGS Σ, !brandidxG Σ}.
   Implicit Types (q : Qp) (α : lft) (γ : gname) (n m : nat).
   Local Notation iProp := (iProp Σ).
 
@@ -158,7 +158,7 @@ Section brandedvec.
 End brandedvec.
 
 Section typing.
-  Context `{!typeG Σ, !brandidxG Σ}.
+  Context `{!typeGS Σ, !brandidxG Σ}.
   Implicit Types (q : Qp) (α : lft) (γ : gname) (n m : nat).
   Local Notation iProp := (iProp Σ).
 
diff --git a/theories/typing/lib/cell.v b/theories/typing/lib/cell.v
index 213fa339ce587a3979b3666fbc4f150e2ec33cf1..9645ecbd03242b0d964497cf481cf8f6e99c7340 100644
--- a/theories/typing/lib/cell.v
+++ b/theories/typing/lib/cell.v
@@ -6,7 +6,7 @@ From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
 Section cell.
-  Context `{!typeG Σ}.
+  Context `{!typeGS Σ}.
 
   Program Definition cell (ty : type) :=
     {| ty_size := ty.(ty_size);
@@ -79,7 +79,7 @@ Section cell.
 End cell.
 
 Section typing.
-  Context `{!typeG Σ}.
+  Context `{!typeGS Σ}.
 
   (** The next couple functions essentially show owned-type equalities, as they
       are all different types for the identity function. *)
diff --git a/theories/typing/lib/diverging_static.v b/theories/typing/lib/diverging_static.v
index 1c985a36742b5f30668cad9db79d47bd486c5662..abbedcab02b3877b3e34de722c727fd87bc77433 100644
--- a/theories/typing/lib/diverging_static.v
+++ b/theories/typing/lib/diverging_static.v
@@ -4,7 +4,7 @@ From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
 Section diverging_static.
-  Context `{!typeG Σ}.
+  Context `{!typeGS Σ}.
 
   (* Show that we can convert any live borrow to 'static with an infinite
      loop. *)
diff --git a/theories/typing/lib/fake_shared.v b/theories/typing/lib/fake_shared.v
index 0b3db02beed2185a7989b9c84594963b53f295ae..d10fe83f204d0427a8b9caa8881f4c70120a6b4a 100644
--- a/theories/typing/lib/fake_shared.v
+++ b/theories/typing/lib/fake_shared.v
@@ -3,7 +3,7 @@ From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
 Section fake_shared.
-  Context `{!typeG Σ}.
+  Context `{!typeGS Σ}.
 
   Definition fake_shared_box : val :=
     fn: ["x"] := Skip ;; return: ["x"].
diff --git a/theories/typing/lib/ghostcell.v b/theories/typing/lib/ghostcell.v
index cbdc1d3856b491718201c379fe29c2b2d2c9416a..7085874bde001bff6df59ec16ce72c62070ec8c3 100644
--- a/theories/typing/lib/ghostcell.v
+++ b/theories/typing/lib/ghostcell.v
@@ -93,7 +93,7 @@ Definition ghosttoken_st_to_R (st : ghosttoken_st) : ghosttoken_stR :=
         end).
 
 Section ghostcell.
-  Context `{!typeG Σ, !ghostcellG Σ}.
+  Context `{!typeGS Σ, !ghostcellG Σ}.
   Implicit Types (α β: lft) (γ: gname) (q: Qp) (ty: type) (l: loc).
 
   Local Instance ghosttoken_fractional γ κ' :
diff --git a/theories/typing/lib/join.v b/theories/typing/lib/join.v
index 9de2211b4b52804c4fef43ef2e43962193b41117..fc593c245e758395d6910872a0d9dc712d2a4280 100644
--- a/theories/typing/lib/join.v
+++ b/theories/typing/lib/join.v
@@ -7,7 +7,7 @@ Set Default Proof Using "Type".
 Definition joinN := lrustN .@ "join".
 
 Section join.
-  Context `{!typeG Σ, !spawnG Σ}.
+  Context `{!typeGS Σ, !spawnG Σ}.
 
   (* This model is very far from rayon::join, which uses a persistent
      work-stealing thread-pool.  Still, the important bits are right:
diff --git a/theories/typing/lib/mutex/mutex.v b/theories/typing/lib/mutex/mutex.v
index f6a5a350054bc9c3cb1729edc64a7588d677d240..ca3cd06d6e12082bbea321f95ad3c31aa5f6ab5c 100644
--- a/theories/typing/lib/mutex/mutex.v
+++ b/theories/typing/lib/mutex/mutex.v
@@ -9,7 +9,7 @@ Set Default Proof Using "Type".
 Definition mutexN := lrustN .@ "mutex".
 
 Section mutex.
-  Context `{!typeG Σ}.
+  Context `{!typeGS Σ}.
 
   (*
     pub struct Mutex<T: ?Sized> {
@@ -126,7 +126,7 @@ Section mutex.
 End mutex.
 
 Section code.
-  Context `{!typeG Σ}.
+  Context `{!typeGS Σ}.
 
   Definition mutex_new ty : val :=
     fn: ["x"] :=
diff --git a/theories/typing/lib/mutex/mutexguard.v b/theories/typing/lib/mutex/mutexguard.v
index 2ca7e007c293353579d63266da7192d11a9b7c07..960c7464935f3b863c125fb94b03ffce6b6f91f6 100644
--- a/theories/typing/lib/mutex/mutexguard.v
+++ b/theories/typing/lib/mutex/mutexguard.v
@@ -16,7 +16,7 @@ Set Default Proof Using "Type".
 *)
 
 Section mguard.
-  Context `{!typeG Σ}.
+  Context `{!typeGS Σ}.
 
   (*
     pub struct MutexGuard<'a, T: ?Sized + 'a> {
@@ -143,7 +143,7 @@ Section mguard.
 End mguard.
 
 Section code.
-  Context `{!typeG Σ}.
+  Context `{!typeGS Σ}.
 
   Lemma mutex_acc E l ty tid q α κ :
     ↑lftN ⊆ E → ↑mutexN ⊆ E →
diff --git a/theories/typing/lib/option.v b/theories/typing/lib/option.v
index 66c6d79b7d91b64756aede9d73f14505b48eddb6..6f7a4b5f2df3d66d3191c379340823630da44614 100644
--- a/theories/typing/lib/option.v
+++ b/theories/typing/lib/option.v
@@ -3,7 +3,7 @@ From lrust.typing Require Import typing lib.panic.
 Set Default Proof Using "Type".
 
 Section option.
-  Context `{!typeG Σ}.
+  Context `{!typeGS Σ}.
 
   Definition option (τ : type) := Σ[unit; τ]%T.
 
diff --git a/theories/typing/lib/panic.v b/theories/typing/lib/panic.v
index f5564c57ba904fc61ff64bd69d2c24a4ca63cc48..fe40d55b118ff1e3d776951806cd8729cbd76ddb 100644
--- a/theories/typing/lib/panic.v
+++ b/theories/typing/lib/panic.v
@@ -11,7 +11,7 @@ Set Default Proof Using "Type".
    [take_mut]. *)
 
 Section panic.
-  Context `{!typeG Σ}.
+  Context `{!typeGS Σ}.
 
   Definition panic : val :=
     fn: [] := #☠.
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index e2ed4647477cfce84bb80db1a36d93fd0006b868..2f7258297352c295b1602c694df55ea3b5d778d8 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -25,7 +25,7 @@ Definition rc_invN := rcN .@ "inv".
 Definition rc_shrN := rcN .@ "shr".
 
 Section rc.
-  Context `{!typeG Σ, !rcG Σ}.
+  Context `{!typeGS Σ, !rcG Σ}.
 
   (* The RC can be in four different states :
        - The living state, meaning that some strong reference exists. The
@@ -236,7 +236,7 @@ Section rc.
 End rc.
 
 Section code.
-  Context `{!typeG Σ, !rcG Σ}.
+  Context `{!typeGS Σ, !rcG Σ}.
 
   Lemma rc_check_unique ty F tid (l : loc) :
     ↑rc_invN ⊆ F →
diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v
index dfea77e5d76f7cbfae005a429ce72d38cf44a792..a218e1de61bbc9203de3c16b75ecfa4945641c99 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -8,7 +8,7 @@ From lrust.typing.lib Require Export rc.
 Set Default Proof Using "Type".
 
 Section weak.
-  Context `{!typeG Σ, !rcG Σ}.
+  Context `{!typeGS Σ, !rcG Σ}.
 
   Program Definition weak (ty : type) :=
     {| ty_size := 1;
@@ -103,7 +103,7 @@ Section weak.
 End weak.
 
 Section code.
-  Context `{!typeG Σ, !rcG Σ}.
+  Context `{!typeGS Σ, !rcG Σ}.
 
   Definition rc_upgrade : val :=
     fn: ["w"] :=
diff --git a/theories/typing/lib/refcell/ref.v b/theories/typing/lib/refcell/ref.v
index e146334c1990343d05856b66c3bc6da97649a5ad..7ee34cc9fc753e340fb973b040318148c89f6c8c 100644
--- a/theories/typing/lib/refcell/ref.v
+++ b/theories/typing/lib/refcell/ref.v
@@ -9,7 +9,7 @@ Set Default Proof Using "Type".
 Definition refcell_refN := refcellN .@ "ref".
 
 Section ref.
-  Context `{!typeG Σ, !refcellG Σ}.
+  Context `{!typeGS Σ, !refcellG Σ}.
 
   (* The Rust type looks as follows (after some unfolding):
 
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index a77c45b8ce2cfb03e778c86f3473405273c80cea..9df46b272a58e9c488d908b8a8bf3934f622d053 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -7,7 +7,7 @@ From lrust.typing.lib.refcell Require Import refcell ref.
 Set Default Proof Using "Type".
 
 Section ref_functions.
-  Context `{!typeG Σ, !refcellG Σ}.
+  Context `{!typeGS Σ, !refcellG Σ}.
 
   Lemma refcell_inv_reading_inv tid l γ α ty q ν :
     refcell_inv tid l γ α ty -∗
diff --git a/theories/typing/lib/refcell/refcell.v b/theories/typing/lib/refcell/refcell.v
index 72219bfa2efdb0dd75c56ebf90c224b43a1f5d8f..15ffbb559ab335ed417e8c11b61a8b34c5d67e97 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -40,7 +40,7 @@ Definition refcellN := lrustN .@ "refcell".
 Definition refcell_invN := refcellN .@ "inv".
 
 Section refcell_inv.
-  Context `{!typeG Σ, !refcellG Σ}.
+  Context `{!typeGS Σ, !refcellG Σ}.
 
   Definition refcell_inv tid (l : loc) (γ : gname) (α : lft) ty : iProp Σ :=
     (∃ st, l ↦ #(Z_of_refcell_st st) ∗ own γ (● (refcell_st_to_R st)) ∗
@@ -94,7 +94,7 @@ Section refcell_inv.
 End refcell_inv.
 
 Section refcell.
-  Context `{!typeG Σ, !refcellG Σ}.
+  Context `{!typeGS Σ, !refcellG Σ}.
 
   (* Original Rust type:
      pub struct RefCell<T: ?Sized> {
diff --git a/theories/typing/lib/refcell/refcell_code.v b/theories/typing/lib/refcell/refcell_code.v
index 17320a4946e3e873f6e38b20aceab30dc68fec4d..a4e20122748d4e188c909e6dc68f15224953c4fb 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -8,7 +8,7 @@ From lrust.typing.lib.refcell Require Import refcell ref refmut.
 Set Default Proof Using "Type".
 
 Section refcell_functions.
-  Context `{!typeG Σ, !refcellG Σ}.
+  Context `{!typeGS Σ, !refcellG Σ}.
 
   (* Constructing a refcell. *)
   Definition refcell_new ty : val :=
diff --git a/theories/typing/lib/refcell/refmut.v b/theories/typing/lib/refcell/refmut.v
index ff6e32e052f9d43d741d7d1e185d144127816dd7..b405995b96879acac27d3134e72df0640337713a 100644
--- a/theories/typing/lib/refcell/refmut.v
+++ b/theories/typing/lib/refcell/refmut.v
@@ -7,7 +7,7 @@ From lrust.typing.lib.refcell Require Import refcell.
 Set Default Proof Using "Type".
 
 Section refmut.
-  Context `{!typeG Σ, !refcellG Σ}.
+  Context `{!typeGS Σ, !refcellG Σ}.
 
   (* The Rust type looks as follows (after some unfolding):
 
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index 4dc1d3bd17825f81b81d1f71062592624284fef8..680c7d77d9d4ee1069b0db88b60947e3e13690f5 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -7,7 +7,7 @@ From lrust.typing.lib.refcell Require Import refcell refmut.
 Set Default Proof Using "Type".
 
 Section refmut_functions.
-  Context `{!typeG Σ, !refcellG Σ}.
+  Context `{!typeGS Σ, !refcellG Σ}.
 
   (* Turning a refmut into a shared borrow. *)
   Definition refmut_deref : val :=
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index e658e08d1b4bbee7c2f733be0fe9e53387bb0c81..ad9ef92c312820867baa75a6c9d0c4f4b0f8f176 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -28,7 +28,7 @@ Definition writing_st : rwlock_stR :=
 Definition rwlockN := lrustN .@ "rwlock".
 
 Section rwlock_inv.
-  Context `{!typeG Σ, !rwlockG Σ}.
+  Context `{!typeGS Σ, !rwlockG Σ}.
 
   Definition rwlock_inv tid_own tid_shr (l : loc) (γ : gname) (α : lft) ty
     : iProp Σ :=
@@ -103,7 +103,7 @@ Section rwlock_inv.
 End rwlock_inv.
 
 Section rwlock.
-  Context `{!typeG Σ, !rwlockG Σ}.
+  Context `{!typeGS Σ, !rwlockG Σ}.
 
   (* Original Rust type (we ignore poisoning):
      pub struct RwLock<T: ?Sized> {
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index 0a86013d747ea809a14973b5864ad96aec465559..2f0f3fcfc8e59bfa997a72ae3646fe9611c42898 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -8,7 +8,7 @@ From lrust.typing.lib.rwlock Require Import rwlock rwlockreadguard rwlockwritegu
 Set Default Proof Using "Type".
 
 Section rwlock_functions.
-  Context `{!typeG Σ, !rwlockG Σ}.
+  Context `{!typeGS Σ, !rwlockG Σ}.
 
   (* Constructing a rwlock. *)
   Definition rwlock_new ty : val :=
diff --git a/theories/typing/lib/rwlock/rwlockreadguard.v b/theories/typing/lib/rwlock/rwlockreadguard.v
index d94c4ab85f4ae2e636ff14fba86c6ac65d89924f..51df1e84e91298de8dd1e0fdf60bda6cd2fb83f0 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard.v
@@ -7,7 +7,7 @@ From lrust.typing.lib.rwlock Require Import rwlock.
 Set Default Proof Using "Type".
 
 Section rwlockreadguard.
-  Context `{!typeG Σ, !rwlockG Σ}.
+  Context `{!typeGS Σ, !rwlockG Σ}.
 
   (* Original Rust type:
     pub struct RwLockReadGuard<'a, T: ?Sized + 'a> {
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index e5ac1c55c47d3a7afd40fa6913bf9ca726b2faee..e2c0553d8920c817ac8a5b3ef5566796a9677e32 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -7,7 +7,7 @@ From lrust.typing.lib.rwlock Require Import rwlock rwlockreadguard.
 Set Default Proof Using "Type".
 
 Section rwlockreadguard_functions.
-  Context `{!typeG Σ, !rwlockG Σ}.
+  Context `{!typeGS Σ, !rwlockG Σ}.
 
   (* Turning a rwlockreadguard into a shared borrow. *)
   Definition rwlockreadguard_deref : val :=
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard.v b/theories/typing/lib/rwlock/rwlockwriteguard.v
index f6ba19e93bf3689907f4c15b46cc800d6764e2c4..702201bc7561fd202e987376fb7a47430c1d2f0e 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard.v
@@ -7,7 +7,7 @@ From lrust.typing.lib.rwlock Require Import rwlock.
 Set Default Proof Using "Type".
 
 Section rwlockwriteguard.
-  Context `{!typeG Σ, !rwlockG Σ}.
+  Context `{!typeGS Σ, !rwlockG Σ}.
 
   (* Original Rust type (we ignore poisoning):
       pub struct RwLockWriteGuard<'a, T: ?Sized + 'a> {
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard_code.v b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
index 8dfc98913d117aac5534d6641ad9b9c5b087c435..beda5f49e0e54248a91872c0f51581e703cd585c 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
@@ -7,7 +7,7 @@ From lrust.typing.lib.rwlock Require Import rwlock rwlockwriteguard.
 Set Default Proof Using "Type".
 
 Section rwlockwriteguard_functions.
-  Context `{!typeG Σ, !rwlockG Σ}.
+  Context `{!typeGS Σ, !rwlockG Σ}.
 
   (* Turning a rwlockwriteguard into a shared borrow. *)
   Definition rwlockwriteguard_deref : val :=
diff --git a/theories/typing/lib/spawn.v b/theories/typing/lib/spawn.v
index f2d2859e5f260f5f4b6776cb7d086fef616f26ef..421bb191bd4dba82038f5e57749a439bb1bd957c 100644
--- a/theories/typing/lib/spawn.v
+++ b/theories/typing/lib/spawn.v
@@ -7,7 +7,7 @@ Set Default Proof Using "Type".
 Definition spawnN := lrustN .@ "spawn".
 
 Section join_handle.
-  Context `{!typeG Σ, !spawnG Σ}.
+  Context `{!typeGS Σ, !spawnG Σ}.
 
   Definition join_inv (ty : type) (v : val) :=
     (∀ tid, (box ty).(ty_own) tid [v])%I.
@@ -65,7 +65,7 @@ Section join_handle.
 End join_handle.
 
 Section spawn.
-  Context `{!typeG Σ, !spawnG Σ}.
+  Context `{!typeGS Σ, !spawnG Σ}.
 
   Definition spawn (call_once : val) : val :=
     fn: ["f"] :=
diff --git a/theories/typing/lib/swap.v b/theories/typing/lib/swap.v
index b6d4cb182c0dfb934f17e1108e064fd5e0e2f2fb..d920a7d2a93ae9b8f5277142137d616bcbf17fd5 100644
--- a/theories/typing/lib/swap.v
+++ b/theories/typing/lib/swap.v
@@ -4,7 +4,7 @@ From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
 Section swap.
-  Context `{!typeG Σ}.
+  Context `{!typeGS Σ}.
 
   Definition swap ty : val :=
     fn: ["p1"; "p2"] :=
diff --git a/theories/typing/lib/take_mut.v b/theories/typing/lib/take_mut.v
index 9adb5ff76498be29678dac6cbd3881a60950f32e..8c9f215563c79c6982a618994913c253907d3e2d 100644
--- a/theories/typing/lib/take_mut.v
+++ b/theories/typing/lib/take_mut.v
@@ -6,7 +6,7 @@ From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
 Section code.
-  Context `{!typeG Σ}.
+  Context `{!typeGS Σ}.
 
   Definition take ty (call_once : val) : val :=
     fn: ["x"; "f"] :=
diff --git a/theories/typing/own.v b/theories/typing/own.v
index a03beedfe019966daaf34404c563faf4553d7a4f..757e883c726a2e82fdf0dd81018ab2891fe67f08 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -5,7 +5,7 @@ From lrust.typing Require Import util uninit type_context programs.
 Set Default Proof Using "Type".
 
 Section own.
-  Context `{!typeG Σ}.
+  Context `{!typeGS Σ}.
 
   Definition freeable_sz (n : nat) (sz : nat) (l : loc) : iProp Σ :=
     match sz, n return _ with
@@ -146,7 +146,7 @@ Section own.
 End own.
 
 Section box.
-  Context `{!typeG Σ}.
+  Context `{!typeGS Σ}.
 
   Definition box ty := own_ptr ty.(ty_size) ty.
 
@@ -183,7 +183,7 @@ Section box.
 End box.
 
 Section util.
-  Context `{!typeG Σ}.
+  Context `{!typeGS Σ}.
 
   Lemma ownptr_own n ty tid v :
     (own_ptr n ty).(ty_own) tid [v] ⊣⊢
@@ -214,7 +214,7 @@ Section util.
 End util.
 
 Section typing.
-  Context `{!typeG Σ}.
+  Context `{!typeGS Σ}.
 
   (** Typing *)
   Lemma write_own {E L} ty ty' n :
diff --git a/theories/typing/product.v b/theories/typing/product.v
index 90f273cd3e1cae6a776ddab8682c2ca5989d68ea..57e1e108a96160bb2a7ff1b3c6d2558b0c5e807e 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -5,7 +5,7 @@ From lrust.typing Require Export type.
 Set Default Proof Using "Type".
 
 Section product.
-  Context `{!typeG Σ}.
+  Context `{!typeGS Σ}.
 
   (* TODO: Find a better spot for this. *)
   Lemma Z_nat_add (n1 n2 : nat) : Z.to_nat (n1 + n2) = (n1 + n2)%nat.
@@ -195,7 +195,7 @@ End product.
 Notation Π := product.
 
 Section typing.
-  Context `{!typeG Σ}.
+  Context `{!typeGS Σ}.
 
   Global Instance prod2_assoc E L : Assoc (eqtype E L) product2.
   Proof.
diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index 3dc9c1ce783ffdda4a9970cefad108e1cce18df3..150710d303db747ace46c3944c126fdecad3816d 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -6,7 +6,7 @@ From lrust.typing Require Import shr_bor.
 Set Default Proof Using "Type".
 
 Section product_split.
-  Context `{!typeG Σ}.
+  Context `{!typeGS Σ}.
 
   (** General splitting / merging for pointer types *)
   Fixpoint hasty_ptr_offsets (p : path) (ptr: type → type) tyl (off : nat) : tctx :=
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index d3e564c7daf85c22a2d0ca798291bad818ec3d6f..f0448ba9ace437bd2894214bb019212d291a094e 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -3,7 +3,7 @@ From lrust.typing Require Export type lft_contexts type_context cont_context.
 Set Default Proof Using "Type".
 
 Section typing.
-  Context `{!typeG Σ}.
+  Context `{!typeGS Σ}.
 
   (** Function Body *)
   (* This is an iProp because it is also used by the function type. *)
@@ -101,17 +101,17 @@ Section typing.
   Proof. rewrite typed_read_eq. apply _. Qed.
 End typing.
 
-Definition typed_instruction_ty `{!typeG Σ} (E : elctx) (L : llctx) (T : tctx)
+Definition typed_instruction_ty `{!typeGS Σ} (E : elctx) (L : llctx) (T : tctx)
     (e : expr) (ty : type) : iProp Σ :=
   typed_instruction E L T e (λ v, [v ◁ ty]).
 Arguments typed_instruction_ty {_ _} _ _ _ _%E _%T.
 
-Definition typed_val `{!typeG Σ} (v : val) (ty : type) : Prop :=
+Definition typed_val `{!typeGS Σ} (v : val) (ty : type) : Prop :=
   ∀ E L, ⊢ typed_instruction_ty E L [] (of_val v) ty.
 Arguments typed_val _ _ _%V _%T.
 
 Section typing_rules.
-  Context `{!typeG Σ}.
+  Context `{!typeGS Σ}.
 
   (* This lemma is helpful when switching from proving unsafe code in Iris
      back to proving it in the type system. *)
diff --git a/theories/typing/shr_bor.v b/theories/typing/shr_bor.v
index e6042d95081afc2f6a9713cb8924718d801f90f2..0fb7bf7fbbff4630d74f866a0d9e95d9d5d4c79b 100644
--- a/theories/typing/shr_bor.v
+++ b/theories/typing/shr_bor.v
@@ -4,7 +4,7 @@ From lrust.typing Require Import lft_contexts type_context programs.
 Set Default Proof Using "Type".
 
 Section shr_bor.
-  Context `{!typeG Σ}.
+  Context `{!typeGS Σ}.
 
   Program Definition shr_bor (κ : lft) (ty : type) : type :=
     {| st_own tid vl :=
@@ -61,7 +61,7 @@ End shr_bor.
 Notation "&shr{ κ }" := (shr_bor κ) (format "&shr{ κ }") : lrust_type_scope.
 
 Section typing.
-  Context `{!typeG Σ}.
+  Context `{!typeGS Σ}.
 
   Lemma shr_mono' E L κ1 κ2 ty1 ty2 :
     lctx_lft_incl E L κ2 κ1 → subtype E L ty1 ty2 →
diff --git a/theories/typing/soundness.v b/theories/typing/soundness.v
index 4280bcf9f0a69584e8cdabd27207b17f80bf6c80..4ef123dcf5af20aa4e3947cb4d3728a7f96b0319 100644
--- a/theories/typing/soundness.v
+++ b/theories/typing/soundness.v
@@ -7,25 +7,25 @@ From lrust.typing Require Import typing.
 
 Set Default Proof Using "Type".
 
-Class typePreG Σ := PreTypeG {
-  type_preG_lrustG :> lrustPreG Σ;
-  type_preG_lftG :> lftPreG Σ;
+Class typeGpreS Σ := PreTypeG {
+  type_preG_lrustGS :> lrustGpreS Σ;
+  type_preG_lftGS :> lftGpreS Σ;
   type_preG_na_invG :> na_invG Σ;
   type_preG_frac_borG :> frac_borG Σ
 }.
 
 Definition typeΣ : gFunctors :=
   #[lrustΣ; lftΣ; na_invΣ; GFunctor (constRF fracR)].
-Instance subG_typePreG {Σ} : subG typeΣ Σ → typePreG Σ.
+Instance subG_typeGpreS {Σ} : subG typeΣ Σ → typeGpreS Σ.
 Proof. solve_inG. Qed.
 
 Section type_soundness.
   Definition exit_cont : val := λ: [<>], #☠.
 
-  Definition main_type `{!typeG Σ} := (fn(∅) → unit)%T.
+  Definition main_type `{!typeGS Σ} := (fn(∅) → unit)%T.
 
-  Theorem type_soundness `{!typePreG Σ} (main : val) σ t :
-    (∀ `{!typeG Σ}, typed_val main main_type) →
+  Theorem type_soundness `{!typeGpreS Σ} (main : val) σ t :
+    (∀ `{!typeGS Σ}, typed_val main main_type) →
     rtc erased_step ([main [exit_cont]%E], ∅) (t, σ) →
     nonracing_threadpool t σ ∧
     (∀ e, e ∈ t → is_Some (to_val e) ∨ reducible e σ).
@@ -63,7 +63,7 @@ End type_soundness.
 (* Soundness theorem when no other CMRA is needed. *)
 
 Theorem type_soundness_closed (main : val) σ t :
-  (∀ `{!typeG typeΣ}, typed_val main main_type) →
+  (∀ `{!typeGS typeΣ}, typed_val main main_type) →
   rtc erased_step ([main [exit_cont]%E], ∅) (t, σ) →
   nonracing_threadpool t σ ∧
   (∀ e, e ∈ t → is_Some (to_val e) ∨ reducible e σ).
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index e68edb4fa5318d43e957519dd836bfef7a416ff4..0bfaa42a954798e3e3c78828964d4f5e563e9532 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -6,7 +6,7 @@ From lrust.typing Require Export type.
 Set Default Proof Using "Type".
 
 Section sum.
-  Context `{!typeG Σ}.
+  Context `{!typeGS Σ}.
 
   (* We define the actual empty type as being the empty sum, so that it is
      convertible to it---and in particular, we can pattern-match on it
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 09cb325cae62ce7f7bccdb2400b50db9e2e0432d..ea9fa41395074bbca4ac58566f9c39cf776a0b2b 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -6,9 +6,9 @@ From lrust.typing Require Export base.
 From lrust.typing Require Import lft_contexts.
 Set Default Proof Using "Type".
 
-Class typeG Σ := TypeG {
-  type_lrustG :> lrustG Σ;
-  type_lftG :> lftG Σ lft_userE;
+Class typeGS Σ := TypeG {
+  type_lrustGS :> lrustGS Σ;
+  type_lftGS :> lftGS Σ lft_userE;
   type_na_invG :> na_invG Σ;
   type_frac_borrowG :> frac_borG Σ
 }.
@@ -18,7 +18,7 @@ Definition shrN  := lrustN .@ "shr".
 
 Definition thread_id := na_inv_pool_name.
 
-Record type `{!typeG Σ} :=
+Record type `{!typeGS Σ} :=
   { ty_size : nat;
     ty_own : thread_id → list val → iProp Σ;
     ty_shr : lft → thread_id → loc → iProp Σ;
@@ -52,14 +52,14 @@ Instance: Params (@ty_shr) 2 := {}.
 
 Arguments ty_own {_ _} !_ _ _ / : simpl nomatch.
 
-Class TyWf `{!typeG Σ} (ty : type) := { ty_lfts : list lft; ty_wf_E : elctx }.
+Class TyWf `{!typeGS Σ} (ty : type) := { ty_lfts : list lft; ty_wf_E : elctx }.
 Arguments ty_lfts {_ _} _ {_}.
 Arguments ty_wf_E {_ _} _ {_}.
 
-Definition ty_outlives_E `{!typeG Σ} ty `{!TyWf ty} (κ : lft) : elctx :=
+Definition ty_outlives_E `{!typeGS Σ} ty `{!TyWf ty} (κ : lft) : elctx :=
   (λ α, κ ⊑ₑ α) <$> ty.(ty_lfts).
 
-Lemma ty_outlives_E_elctx_sat `{!typeG Σ} E L ty `{!TyWf ty} α β :
+Lemma ty_outlives_E_elctx_sat `{!typeGS Σ} E L ty `{!TyWf ty} α β :
   ty_outlives_E ty β ⊆+ E →
   lctx_lft_incl E L α β →
   elctx_sat E L (ty_outlives_E ty α).
@@ -73,34 +73,34 @@ Proof.
 Qed.
 
 (* Lift TyWf to lists.  We cannot use `Forall` because that one is restricted to Prop. *)
-Inductive ListTyWf `{!typeG Σ} : list type → Type :=
+Inductive ListTyWf `{!typeGS Σ} : list type → Type :=
 | list_ty_wf_nil : ListTyWf []
 | list_ty_wf_cons ty tyl `{!TyWf ty, !ListTyWf tyl} : ListTyWf (ty::tyl).
 Existing Class ListTyWf.
 Existing Instances list_ty_wf_nil list_ty_wf_cons.
 
-Fixpoint tyl_lfts `{!typeG Σ} tyl {WF : ListTyWf tyl} : list lft :=
+Fixpoint tyl_lfts `{!typeGS Σ} tyl {WF : ListTyWf tyl} : list lft :=
   match WF with
   | list_ty_wf_nil => []
   | list_ty_wf_cons ty [] => ty.(ty_lfts)
   | list_ty_wf_cons ty tyl => ty.(ty_lfts) ++ tyl.(tyl_lfts)
   end.
 
-Fixpoint tyl_wf_E `{!typeG Σ} tyl {WF : ListTyWf tyl} : elctx :=
+Fixpoint tyl_wf_E `{!typeGS Σ} tyl {WF : ListTyWf tyl} : elctx :=
   match WF with
   | list_ty_wf_nil => []
   | list_ty_wf_cons ty [] => ty.(ty_wf_E)
   | list_ty_wf_cons ty tyl => ty.(ty_wf_E) ++ tyl.(tyl_wf_E)
   end.
 
-Fixpoint tyl_outlives_E `{!typeG Σ} tyl {WF : ListTyWf tyl} (κ : lft) : elctx :=
+Fixpoint tyl_outlives_E `{!typeGS Σ} tyl {WF : ListTyWf tyl} (κ : lft) : elctx :=
   match WF with
   | list_ty_wf_nil => []
   | list_ty_wf_cons ty [] => ty_outlives_E ty κ
   | list_ty_wf_cons ty tyl => ty_outlives_E ty κ ++ tyl.(tyl_outlives_E) κ
   end.
 
-Lemma tyl_outlives_E_elctx_sat `{!typeG Σ} E L tyl {WF : ListTyWf tyl} α β :
+Lemma tyl_outlives_E_elctx_sat `{!typeGS Σ} E L tyl {WF : ListTyWf tyl} α β :
   tyl_outlives_E tyl β ⊆+ E →
   lctx_lft_incl E L α β →
   elctx_sat E L (tyl_outlives_E tyl α).
@@ -112,14 +112,14 @@ Proof.
       (etrans; [|done]); solve_typing.
 Qed.
 
-Record simple_type `{!typeG Σ} :=
+Record simple_type `{!typeGS Σ} :=
   { st_own : thread_id → list val → iProp Σ;
     st_size_eq tid vl : st_own tid vl -∗ ⌜length vl = 1%nat⌝;
     st_own_persistent tid vl : Persistent (st_own tid vl) }.
 Existing Instance st_own_persistent.
 Instance: Params (@st_own) 2 := {}.
 
-Program Definition ty_of_st `{!typeG Σ} (st : simple_type) : type :=
+Program Definition ty_of_st `{!typeGS Σ} (st : simple_type) : type :=
   {| ty_size := 1; ty_own := st.(st_own);
      (* [st.(st_own) tid vl] needs to be outside of the fractured
          borrow, otherwise I do not know how to prove the shr part of
@@ -149,7 +149,7 @@ Bind Scope lrust_type_scope with type.
 
 (* OFE and COFE structures on types and simple types. *)
 Section ofe.
-  Context `{!typeG Σ}.
+  Context `{!typeGS Σ}.
 
   Inductive type_equiv' (ty1 ty2 : type) : Prop :=
     Type_equiv :
@@ -260,7 +260,7 @@ End ofe.
 
 (** Special metric for type-nonexpansive and Type-contractive functions. *)
 Section type_dist2.
-  Context `{!typeG Σ}.
+  Context `{!typeGS Σ}.
 
   (* Size and shr are n-equal, but own is only n-1-equal.
      We need this to express what shr has to satisfy on a Type-NE-function:
@@ -328,7 +328,7 @@ Notation TypeNonExpansive T := (∀ n, Proper (type_dist2 n ==> type_dist2 n) T)
 Notation TypeContractive T := (∀ n, Proper (type_dist2_later n ==> type_dist2 n) T).
 
 Section type_contractive.
-  Context `{!typeG Σ}.
+  Context `{!typeGS Σ}.
 
   Lemma type_ne_dist_later T :
     TypeNonExpansive T → ∀ n, Proper (type_dist2_later n ==> type_dist2_later n) T.
@@ -389,7 +389,7 @@ Fixpoint shr_locsE (l : loc) (n : nat) : coPset :=
   | S n => ↑shrN.@l ∪ shr_locsE (l +ₗ 1%nat) n
   end.
 
-Class Copy `{!typeG Σ} (t : type) := {
+Class Copy `{!typeGS Σ} (t : type) := {
   copy_persistent tid vl : Persistent (t.(ty_own) tid vl);
   copy_shr_acc κ tid E F l q :
     ↑lftN ∪ ↑shrN ⊆ E → shr_locsE l (t.(ty_size) + 1) ⊆ F →
@@ -402,34 +402,34 @@ Class Copy `{!typeG Σ} (t : type) := {
 Existing Instances copy_persistent.
 Instance: Params (@Copy) 2 := {}.
 
-Class ListCopy `{!typeG Σ} (tys : list type) := lst_copy : Forall Copy tys.
+Class ListCopy `{!typeGS Σ} (tys : list type) := lst_copy : Forall Copy tys.
 Instance: Params (@ListCopy) 2 := {}.
-Global Instance lst_copy_nil `{!typeG Σ} : ListCopy [] := List.Forall_nil _.
-Global Instance lst_copy_cons `{!typeG Σ} ty tys :
+Global Instance lst_copy_nil `{!typeGS Σ} : ListCopy [] := List.Forall_nil _.
+Global Instance lst_copy_cons `{!typeGS Σ} ty tys :
   Copy ty → ListCopy tys → ListCopy (ty :: tys) := List.Forall_cons _ _ _.
 
-Class Send `{!typeG Σ} (t : type) :=
+Class Send `{!typeGS Σ} (t : type) :=
   send_change_tid tid1 tid2 vl : t.(ty_own) tid1 vl -∗ t.(ty_own) tid2 vl.
 Instance: Params (@Send) 2 := {}.
 
-Class ListSend `{!typeG Σ} (tys : list type) := lst_send : Forall Send tys.
+Class ListSend `{!typeGS Σ} (tys : list type) := lst_send : Forall Send tys.
 Instance: Params (@ListSend) 2 := {}.
-Global Instance lst_send_nil `{!typeG Σ} : ListSend [] := List.Forall_nil _.
-Global Instance lst_send_cons `{!typeG Σ} ty tys :
+Global Instance lst_send_nil `{!typeGS Σ} : ListSend [] := List.Forall_nil _.
+Global Instance lst_send_cons `{!typeGS Σ} ty tys :
   Send ty → ListSend tys → ListSend (ty :: tys) := List.Forall_cons _ _ _.
 
-Class Sync `{!typeG Σ} (t : type) :=
+Class Sync `{!typeGS Σ} (t : type) :=
   sync_change_tid κ tid1 tid2 l : t.(ty_shr) κ tid1 l -∗ t.(ty_shr) κ tid2 l.
 Instance: Params (@Sync) 2 := {}.
 
-Class ListSync `{!typeG Σ} (tys : list type) := lst_sync : Forall Sync tys.
+Class ListSync `{!typeGS Σ} (tys : list type) := lst_sync : Forall Sync tys.
 Instance: Params (@ListSync) 2 := {}.
-Global Instance lst_sync_nil `{!typeG Σ} : ListSync [] := List.Forall_nil _.
-Global Instance lst_sync_cons `{!typeG Σ} ty tys :
+Global Instance lst_sync_nil `{!typeGS Σ} : ListSync [] := List.Forall_nil _.
+Global Instance lst_sync_cons `{!typeGS Σ} ty tys :
   Sync ty → ListSync tys → ListSync (ty :: tys) := List.Forall_cons _ _ _.
 
 Section type.
-  Context `{!typeG Σ}.
+  Context `{!typeGS Σ}.
 
   (** Copy types *)
   Lemma shr_locsE_shift l n m :
@@ -532,30 +532,30 @@ Section type.
   Qed.
 End type.
 
-Definition type_incl `{!typeG Σ} (ty1 ty2 : type) : iProp Σ :=
+Definition type_incl `{!typeGS Σ} (ty1 ty2 : type) : iProp Σ :=
     (⌜ty1.(ty_size) = ty2.(ty_size)⌝ ∗
      (□ ∀ tid vl, ty1.(ty_own) tid vl -∗ ty2.(ty_own) tid vl) ∗
      (□ ∀ κ tid l, ty1.(ty_shr) κ tid l -∗ ty2.(ty_shr) κ tid l))%I.
 Instance: Params (@type_incl) 2 := {}.
 (* Typeclasses Opaque type_incl. *)
 
-Definition type_equal `{!typeG Σ} (ty1 ty2 : type) : iProp Σ :=
+Definition type_equal `{!typeGS Σ} (ty1 ty2 : type) : iProp Σ :=
     (⌜ty1.(ty_size) = ty2.(ty_size)⌝ ∗
      (□ ∀ tid vl, ty1.(ty_own) tid vl ∗-∗ ty2.(ty_own) tid vl) ∗
      (□ ∀ κ tid l, ty1.(ty_shr) κ tid l ∗-∗ ty2.(ty_shr) κ tid l))%I.
 Instance: Params (@type_equal) 2 := {}.
 
-Definition subtype `{!typeG Σ} (E : elctx) (L : llctx) (ty1 ty2 : type) : Prop :=
+Definition subtype `{!typeGS Σ} (E : elctx) (L : llctx) (ty1 ty2 : type) : Prop :=
   ∀ qmax qL, llctx_interp_noend qmax L qL -∗ □ (elctx_interp E -∗ type_incl ty1 ty2).
 Instance: Params (@subtype) 4 := {}.
 
 (* TODO: The prelude should have a symmetric closure. *)
-Definition eqtype `{!typeG Σ} (E : elctx) (L : llctx) (ty1 ty2 : type) : Prop :=
+Definition eqtype `{!typeGS Σ} (E : elctx) (L : llctx) (ty1 ty2 : type) : Prop :=
   subtype E L ty1 ty2 ∧ subtype E L ty2 ty1.
 Instance: Params (@eqtype) 4 := {}.
 
 Section subtyping.
-  Context `{!typeG Σ}.
+  Context `{!typeGS Σ}.
 
   Global Instance type_incl_ne : NonExpansive2 type_incl.
   Proof.
@@ -742,7 +742,7 @@ Section subtyping.
 End subtyping.
 
 Section type_util.
-  Context `{!typeG Σ}.
+  Context `{!typeGS Σ}.
 
   Lemma heap_mapsto_ty_own l ty tid :
     l ↦∗: ty_own ty tid ⊣⊢ ∃ (vl : vec val ty.(ty_size)), l ↦∗ vl ∗ ty_own ty tid vl.
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index b0fb3cb2477200f9a7107fd972ed7e2f89925743..45da5647a116ca05317862376546c22c8824f7f5 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -7,7 +7,7 @@ Bind Scope expr_scope with path.
 
 (* TODO: Consider making this a pair of a path and the rest. We could
    then e.g. formulate tctx_elt_hasty_path more generally. *)
-Inductive tctx_elt `{!typeG Σ} : Type :=
+Inductive tctx_elt `{!typeGS Σ} : Type :=
 | TCtx_hasty (p : path) (ty : type)
 | TCtx_blocked (p : path) (κ : lft) (ty : type).
 
@@ -18,7 +18,7 @@ Notation "p ◁{ κ } ty" := (TCtx_blocked p κ ty)
    (at level 70, format "p  ◁{ κ }  ty").
 
 Section type_context.
-  Context `{!typeG Σ}.
+  Context `{!typeGS Σ}.
   Implicit Types T : tctx.
 
   Fixpoint eval_path (p : path) : option val :=
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index 5e3dedaf1260220904cb5ea19929e913b1418db4..4bb4ab17cad169854346fd41e54356cee8ff7d8a 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -5,7 +5,7 @@ From lrust.typing Require Import lft_contexts type_context programs product.
 Set Default Proof Using "Type".
 
 Section case.
-  Context `{!typeG Σ}.
+  Context `{!typeGS Σ}.
 
   (* FIXME : have an Iris version of Forall2. *)
   Lemma type_case_own' E L C T p n tyl el :
diff --git a/theories/typing/uninit.v b/theories/typing/uninit.v
index e45318a9f54c9ed7b254e11c4122fc2b9800e55f..23637fd5c25e8708dc00cd7f0030256b1444b407 100644
--- a/theories/typing/uninit.v
+++ b/theories/typing/uninit.v
@@ -4,7 +4,7 @@ From lrust.typing Require Import product.
 Set Default Proof Using "Type".
 
 Section uninit.
-  Context `{!typeG Σ}.
+  Context `{!typeGS Σ}.
 
   Program Definition uninit_1 : type :=
     {| st_own tid vl := ⌜length vl = 1%nat⌝%I |}.
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index f5ca1e03f8ffc49013949cb00ec17684d77db220..3813dd687668b0c23568eb33462f9f854eede474 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -5,7 +5,7 @@ From lrust.typing Require Import util lft_contexts type_context programs.
 Set Default Proof Using "Type".
 
 Section uniq_bor.
-  Context `{!typeG Σ}.
+  Context `{!typeGS Σ}.
 
   Program Definition uniq_bor (κ:lft) (ty:type) :=
     {| ty_size := 1;
@@ -113,7 +113,7 @@ End uniq_bor.
 Notation "&uniq{ κ }" := (uniq_bor κ) (format "&uniq{ κ }") : lrust_type_scope.
 
 Section typing.
-  Context `{!typeG Σ}.
+  Context `{!typeGS Σ}.
 
   Lemma uniq_mono' E L κ1 κ2 ty1 ty2 :
     lctx_lft_incl E L κ2 κ1 → eqtype E L ty1 ty2 →
diff --git a/theories/typing/util.v b/theories/typing/util.v
index 6bf47379bbe0c32b3a0703a7064fbe2cfa12efa0..5edf38b704ce896cc65a10921e86c581d068f94a 100644
--- a/theories/typing/util.v
+++ b/theories/typing/util.v
@@ -3,7 +3,7 @@ From lrust.typing Require Export type.
 Set Default Proof Using "Type".
 
 Section util.
-  Context `{!typeG Σ}.
+  Context `{!typeGS Σ}.
 
   (* Delayed sharing is used by various types; in particular own and uniq.
      It comes in two flavors: Borrows of "later something" and borrows of