update ref files

tests/atomic.ref

 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   aheap : atomic_heap Σ
   Q : iProp Σ
   l : loc
@@ -23,14 +23,14 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   P : val → iProp Σ
   ============================
   ⊢ <<< ∀ x : val, P x >>> code @ ⊤ <<< ∃ y : val, P y, RET #() >>>
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   P : val → iProp Σ
   Φ : language.val heap_lang → iProp Σ
   ============================
@@ -41,7 +41,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   P : val → iProp Σ
   Φ : language.val heap_lang → iProp Σ
   ============================
@@ -55,14 +55,14 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   l : loc
   ============================
   ⊢ <<< ∀ x : val, l ↦ x >>> code @ ⊤ <<< l ↦ x, RET #() >>>
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   l : loc
   Φ : language.val heap_lang → iProp Σ
   ============================
@@ -73,7 +73,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   l : loc
   Φ : language.val heap_lang → iProp Σ
   ============================
@@ -86,14 +86,14 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   l : loc
   ============================
   ⊢ <<< l ↦ #() >>> code @ ⊤ <<< ∃ y : val, l ↦ y, RET #() >>>
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   l : loc
   Φ : language.val heap_lang → iProp Σ
   ============================
@@ -104,7 +104,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   l : loc
   Φ : language.val heap_lang → iProp Σ
   ============================
@@ -118,14 +118,14 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   l : loc
   ============================
   ⊢ <<< l ↦ #() >>> code @ ⊤ <<< l ↦ #(), RET #() >>>
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   l : loc
   Φ : language.val heap_lang → iProp Σ
   ============================
@@ -136,7 +136,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   l : loc
   Φ : language.val heap_lang → iProp Σ
   ============================
@@ -151,7 +151,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   l : loc
   ============================
   ⊢ <<< ∀ x : val, l ↦ x ∗ l ↦ x >>>
@@ -160,7 +160,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   l : loc
   Φ : language.val heap_lang → iProp Σ
   ============================
@@ -172,7 +172,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   l : loc
   ============================
   ⊢ <<< ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
@@ -181,7 +181,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   l : loc
   Φ : language.val heap_lang → iProp Σ
   ============================
@@ -193,7 +193,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   l : loc
   ============================
   ⊢ <<< ∀ xx : val, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
@@ -203,7 +203,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   l : loc
   Φ : language.val heap_lang → iProp Σ
   ============================
@@ -217,7 +217,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   l : loc
   ============================
   ⊢ <<< ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
@@ -226,7 +226,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   l : loc
   Φ : language.val heap_lang → iProp Σ
   ============================
@@ -238,7 +238,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   l : loc
   x : val
   ============================
@@ -248,7 +248,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   l : loc
   x : val
   Φ : language.val heap_lang → iProp Σ
@@ -261,7 +261,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   l : loc
   x : val
   ============================
@@ -271,7 +271,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   l : loc
   x : val
   Φ : language.val heap_lang → iProp Σ
@@ -284,7 +284,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   l : loc
   xx, yyyy : val
   ============================
@@ -294,7 +294,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   l : loc
   xx, yyyy : val
   Φ : language.val heap_lang → iProp Σ
@@ -307,7 +307,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   l : loc
   xx, yyyy : val
   ============================
@@ -318,7 +318,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   l : loc
   xx, yyyy : val
   Φ : language.val heap_lang → iProp Σ
@@ -334,7 +334,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   P : val → iProp Σ
   Φ : language.val heap_lang → iProp Σ
   ============================

tests/heap_lang.ref

@@ -3,7 +3,7 @@
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   E : coPset
   ============================
   --------------------------------------∗
@@ -12,7 +12,7 @@
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   E : coPset
   l : loc
   ============================
@@ -25,7 +25,7 @@
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   E : coPset
   l : loc
   ============================
@@ -37,7 +37,7 @@
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   E : coPset
   l, l' : loc
   ============================
@@ -51,7 +51,7 @@
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   l : loc
   ============================
   _ : ▷ l ↦ #0
@@ -61,7 +61,7 @@
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   l : loc
   ============================
   _ : l ↦ #1
@@ -97,7 +97,7 @@ Tactic failure: wp_bind: cannot find (! ?e)%E in (Val #()).
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   l : loc
   ============================
   "Hl1" : l ↦{#1 / 2} #0
@@ -108,7 +108,7 @@ Tactic failure: wp_bind: cannot find (! ?e)%E in (Val #()).
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   l : loc
   ============================
   --------------------------------------∗
@@ -122,7 +122,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   ============================
   --------------------------------------∗
   WP "x" {{ _, True }}
@@ -130,7 +130,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   n : Z
   H : (0 < n)%Z
   Φ : val → iPropI Σ
@@ -146,7 +146,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   l : loc
   vs : list val
   ============================
@@ -160,7 +160,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   v : val
   ============================
   --------------------------------------∗
@@ -171,7 +171,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   v : val
   ============================
   --------------------------------------∗
@@ -180,7 +180,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   l : loc
   v : val
   Φ : val → iPropI Σ
@@ -194,7 +194,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   dq : dfrac
   l : loc
   v : val
@@ -208,7 +208,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   l : loc
   I : val → Prop
   Heq : ∀ v : val, I v ↔ I #true
@@ -219,7 +219,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
 2 goals
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   E1, E2 : coPset
   P : iProp Σ
   ============================
@@ -235,7 +235,7 @@ WP #() #() @ E2 {{ _, |={E2,E1}=> True }}
 2 goals
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   N : namespace
   E : coPset
   P : iProp Σ
@@ -254,7 +254,7 @@ WP #() #() @ E ∖ ↑N {{ _, |={E ∖ ↑N,E}=> True }}
 2 goals
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   N : namespace
   E : coPset
   P : iProp Σ
@@ -270,7 +270,7 @@ WP #() #() @ E ∖ ↑N {{ _, |={E ∖ ↑N}=> ▷ P ∗ True }}
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   ============================
   --------------------------------------∗
   WP let: "f" := λ: "x", "x" in ref ("f" #10) {{ _, True }}
@@ -278,7 +278,7 @@ WP #() #() @ E ∖ ↑N {{ _, |={E ∖ ↑N}=> ▷ P ∗ True }}
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   fun1, fun2, fun3 : expr
   ============================
   --------------------------------------∗
@@ -290,7 +290,7 @@ WP #() #() @ E ∖ ↑N {{ _, |={E ∖ ↑N}=> ▷ P ∗ True }}
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   fun1, fun2, fun3 : expr
   Φ : language.val heap_lang → iPropI Σ
   ============================
@@ -303,7 +303,7 @@ WP #() #() @ E ∖ ↑N {{ _, |={E ∖ ↑N}=> ▷ P ∗ True }}
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   fun1, fun2, fun3 : expr
   Φ : language.val heap_lang → iPropI Σ
   E : coPset
@@ -317,7 +317,7 @@ WP #() #() @ E ∖ ↑N {{ _, |={E ∖ ↑N}=> ▷ P ∗ True }}
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   fun1, fun2, fun3 : expr
   ============================
   {{{ True }}}

tests/heap_lang2.ref

 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   P, Q : iProp Σ
   ============================
   P ={⊤}=∗ Q
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   fun1, fun2, fun3 : expr
   ============================
   --------------------------------------∗
@@ -20,7 +20,7 @@
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   fun1, fun2, fun3 : expr
   ============================
   {{{ True }}}

tests/ipm_paper.ref

@@ -66,7 +66,7 @@ P
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   counterG0 : counterG Σ
   l : loc
   n : nat
@@ -82,7 +82,7 @@ P
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   counterG0 : counterG Σ
   l : loc
   n : nat

tests/list_reverse.ref

 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   hd, acc : val
   xs, ys : list val
   Φ : val → iPropI Σ
@@ -15,7 +15,7 @@
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   acc : val
   ys : list val
   Φ : val → iPropI Σ

tests/one_shot.ref

 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   one_shotG0 : one_shotG Σ
   Φ : val → iProp Σ
   N : namespace
@@ -20,7 +20,7 @@
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   one_shotG0 : one_shotG Σ
   Φ : val → iProp Σ
   N : namespace

tests/one_shot_once.ref

 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   one_shotG0 : one_shotG Σ
   Φ : val → iProp Σ
   N : namespace
@@ -20,7 +20,7 @@
 1 goal
   
   Σ : gFunctors
-  heapG0 : heapG Σ
+  heapGS0 : heapGS Σ
   one_shotG0 : one_shotG Σ
   Φ : val → iProp Σ
   N : namespace

tests/proofmode_ascii.ref

 1 goal
   
   Σ : gFunctors
-  invG0 : invG Σ
+  invGS0 : invGS Σ
   cinvG0 : cinvG Σ
   na_invG0 : na_invG Σ
   N : namespace
@@ -15,7 +15,7 @@
 1 goal
   
   Σ : gFunctors
-  invG0 : invG Σ
+  invGS0 : invGS Σ
   cinvG0 : cinvG Σ
   na_invG0 : na_invG Σ
   N : namespace
@@ -31,7 +31,7 @@
 1 goal
   
   Σ : gFunctors
-  invG0 : invG Σ
+  invGS0 : invGS Σ
   cinvG0 : cinvG Σ
   na_invG0 : na_invG Σ
   γ : gname
@@ -49,7 +49,7 @@
 1 goal
   
   Σ : gFunctors
-  invG0 : invG Σ
+  invGS0 : invGS Σ
   cinvG0 : cinvG Σ
   na_invG0 : na_invG Σ
   γ : gname
@@ -68,7 +68,7 @@
 1 goal
   
   Σ : gFunctors
-  invG0 : invG Σ
+  invGS0 : invGS Σ
   cinvG0 : cinvG Σ
   na_invG0 : na_invG Σ
   t : na_inv_pool_name
@@ -89,7 +89,7 @@
 1 goal
   
   Σ : gFunctors
-  invG0 : invG Σ
+  invGS0 : invGS Σ
   cinvG0 : cinvG Σ
   na_invG0 : na_invG Σ
   t : na_inv_pool_name
@@ -120,7 +120,7 @@ Tactic failure: iInv: invariant "H2" not found.
 1 goal
   
   Σ : gFunctors
-  invG0 : invG Σ
+  invGS0 : invGS Σ
   I : biIndex
   N : namespace
   E : coPset
@@ -136,7 +136,7 @@ Tactic failure: iInv: invariant "H2" not found.
 1 goal
   
   Σ : gFunctors
-  invG0 : invG Σ
+  invGS0 : invGS Σ
   I : biIndex
   N : namespace
   E : coPset

tests/proofmode_iris.ref

 1 goal
   
   Σ : gFunctors
-  invG0 : invG Σ
+  invGS0 : invGS Σ
   cinvG0 : cinvG Σ
   na_invG0 : na_invG Σ
   N : namespace
@@ -15,7 +15,7 @@
 1 goal
   
   Σ : gFunctors
-  invG0 : invG Σ
+  invGS0 : invGS Σ
   cinvG0 : cinvG Σ
   na_invG0 : na_invG Σ
   N : namespace
@@ -31,7 +31,7 @@
 1 goal
   
   Σ : gFunctors
-  invG0 : invG Σ
+  invGS0 : invGS Σ
   cinvG0 : cinvG Σ
   na_invG0 : na_invG Σ
   γ : gname
@@ -43,7 +43,7 @@
 1 goal
   
   Σ : gFunctors
-  invG0 : invG Σ
+  invGS0 : invGS Σ
   cinvG0 : cinvG Σ
   na_invG0 : na_invG Σ
   γ : gname
@@ -61,7 +61,7 @@
 1 goal
   
   Σ : gFunctors
-  invG0 : invG Σ
+  invGS0 : invGS Σ
   cinvG0 : cinvG Σ
   na_invG0 : na_invG Σ
   γ : gname
@@ -80,7 +80,7 @@
 1 goal
   
   Σ : gFunctors
-  invG0 : invG Σ
+  invGS0 : invGS Σ
   cinvG0 : cinvG Σ
   na_invG0 : na_invG Σ
   t : na_inv_pool_name
@@ -101,7 +101,7 @@
 1 goal
   
   Σ : gFunctors
-  invG0 : invG Σ
+  invGS0 : invGS Σ
   cinvG0 : cinvG Σ
   na_invG0 : na_invG Σ
   t : na_inv_pool_name
@@ -115,7 +115,7 @@
 1 goal
   
   Σ : gFunctors
-  invG0 : invG Σ
+  invGS0 : invGS Σ
   cinvG0 : cinvG Σ
   na_invG0 : na_invG Σ
   t : na_inv_pool_name
@@ -146,7 +146,7 @@ Tactic failure: iInv: invariant "H2" not found.
 1 goal
   
   Σ : gFunctors
-  invG0 : invG Σ
+  invGS0 : invGS Σ
   cinvG0 : cinvG Σ
   na_invG0 : na_invG Σ
   inG0 : inG Σ fracR
@@ -160,7 +160,7 @@ Tactic failure: iInv: invariant "H2" not found.
 1 goal
   
   Σ : gFunctors
-  invG0 : invG Σ
+  invGS0 : invGS Σ
   cinvG0 : cinvG Σ
   na_invG0 : na_invG Σ
   inG0 : inG Σ fracR
@@ -175,7 +175,7 @@ Tactic failure: iInv: invariant "H2" not found.
 1 goal
   
   Σ : gFunctors
-  invG0 : invG Σ
+  invGS0 : invGS Σ
   I : biIndex
   N : namespace
   E : coPset
@@ -191,7 +191,7 @@ Tactic failure: iInv: invariant "H2" not found.
 1 goal
   
   Σ : gFunctors
-  invG0 : invG Σ
+  invGS0 : invGS Σ
   I : biIndex
   N : namespace
   E : coPset

tests/proofmode_monpred.ref

@@ -63,7 +63,7 @@ Tactic failure: iFrame: cannot frame (P i).
   
   I : biIndex
   Σ : gFunctors
-  invG0 : invG Σ
+  invGS0 : invGS Σ
   N : namespace
   𝓟 : iProp Σ
   ============================
@@ -76,7 +76,7 @@ Tactic failure: iFrame: cannot frame (P i).
   
   I : biIndex
   Σ : gFunctors
-  invG0 : invG Σ
+  invGS0 : invGS Σ
   N : namespace
   𝓟 : iProp Σ
   ============================