diff --git a/gpfsl-examples/exchanger/proof_graph_resource.v b/gpfsl-examples/exchanger/proof_graph_resource.v
index 6eec8094a25e5e835bbefe355021ee55eab4ffc2..67fad1332b0a01d9cfb89ffbbfe51fcc259d6d71 100644
--- a/gpfsl-examples/exchanger/proof_graph_resource.v
+++ b/gpfsl-examples/exchanger/proof_graph_resource.v
@@ -127,7 +127,7 @@ Proof.
   { iNext. iExists âˆ…. iFrame. by rewrite /TradeResources big_sepL_nil. }
   iMod ("EL" $! _ (EI  Î³b Î³g P) N) as "EL".
   iIntros "!>". iApply ("Post" $! Î³g).
-  iSplitR "I2"; iFrame. iExists _; iFrame.
+  iSplitR "I2"; iFrame.
 Qed.
 
 Lemma exchanger_resource_spec_derived :
diff --git a/gpfsl-examples/queue/proof_mp2_graph.v b/gpfsl-examples/queue/proof_mp2_graph.v
index b68f5c2c3d953bb83cb37ee54cb1296da73e4457..cabb223a2f3e617a3e9d30003be6924876730208 100644
--- a/gpfsl-examples/queue/proof_mp2_graph.v
+++ b/gpfsl-examples/queue/proof_mp2_graph.v
@@ -112,7 +112,7 @@ Proof using All.
     awp_apply (enqueue_spec with "âŠ’V QL"); [solve_ndisj|done|].
     iInv mpN as (G1) "(FI & QI & >â—m & >â—¯m & >%Hv)".
     iAaccIntro with "QI".
-    { iFrame. iIntros "QI !> !>". iExists _. iFrame. done. }
+    { iFrame. iIntros "QI !> !>". iFrame. done. }
     iIntros (V1 G1' enqId1 enq1 Venq1 M1') "(QI & #âŠ’V1 & #QL1 & %F) !>".
     set (eV1 := mkGraphEvent enq1 Venq1 M1') in *.
     rewrite /is_enqueue in F.
@@ -134,7 +134,7 @@ Proof using All.
     iDestruct (graph_master_snap_included with "Gm Gs") as %SubG1'2.
     iSpecialize ("QI" with "[$Gm]").
     iAaccIntro with "QI".
-    { iFrame. iIntros "QI !> !>". iExists _. iFrame. done. }
+    { iFrame. iIntros "QI !> !>". iFrame. done. }
     iIntros (V2 G2' enqId2 enq2 Venq2 M2') "(QI & #âŠ’V2 & #QL2 & %F) !>".
     set (eV2 := mkGraphEvent enq2 Venq2 M2') in *.
     rewrite /is_enqueue in F.
@@ -184,7 +184,7 @@ Proof using All.
     iInv mpN as (G) "(FI & QI & >â—m & >â—¯m & >%Hv)".
     iDestruct (QueueInv_QueueConsistent with "QI") as "#>%QC".
     iAaccIntro with "QI".
-    { iFrame. iIntros "QI !> !>". iExists _. iFrame. done. }
+    { iFrame. iIntros "QI !> !>". iFrame. done. }
     iIntros (v V' G' enqId deqId enq deq Vdeq M') "(QI & #âŠ’V' & #QL' & %F) !>".
     iSplitL; last by iIntros. iNext. iExists G'.
     set (dV := mkGraphEvent deq Vdeq M') in *.
@@ -289,7 +289,7 @@ Proof using All.
 
   iAaccIntro with "QI".
   { iDestruct "â—¯m" as "[â—¯m $]". iFrame. iIntros "QI !> !>".
-    iExists _. iFrame. done. }
+    iFrame. done. }
 
   iIntros (v V' G' enqId deqId enq deq Vdeq M') "(QI & #âŠ’V' & #QL' & %F)".
   set (dV := mkGraphEvent deq Vdeq M') in *.
diff --git a/gpfsl-examples/queue/proof_ms_abs_graph.v b/gpfsl-examples/queue/proof_ms_abs_graph.v
index 2141fac9c5c619ed0b0ab04eaf90feb2ee3b044a..46ae2beddf1992ea10cb4958c63d1bb45b0b4991 100644
--- a/gpfsl-examples/queue/proof_ms_abs_graph.v
+++ b/gpfsl-examples/queue/proof_ms_abs_graph.v
@@ -1003,7 +1003,7 @@ Proof.
   rewrite /Link. iDestruct 1 as (t0 V0 Î¶) "[AT LR]".
   iDestruct "LR" as (V e v) "(#F1 & #F2 & #SE & LV & NA)".
   iSplitR "NA".
-  - iExists t0, V0, Î¶. iFrame. iExists V, e, v. by iFrame "#âˆ—".
+  - iExists t0, V0, Î¶. iFrame. iExists e, v. by iFrame "#âˆ—".
   - rewrite /seen_enqueued_val /SeenEvent.
     iDestruct "SE" as (eV (Eqv & <- & SE) EqE) "SE". iDestruct "F2" as %EqT.
     iExists e, eV, v. iSplit; [done|]. by iFrame "NA".
diff --git a/gpfsl-examples/queue/proof_spsc_graph.v b/gpfsl-examples/queue/proof_spsc_graph.v
index ddbfbc1a1ce5d705afb8d6648489b3a74ddb6320..5541b28c88c52cbb90d69a1ecb31875437181ce2 100644
--- a/gpfsl-examples/queue/proof_spsc_graph.v
+++ b/gpfsl-examples/queue/proof_spsc_graph.v
@@ -180,7 +180,7 @@ Proof.
   iSpecialize ("QI" with "[$Gm]").
 
   iAaccIntro with "QI".
-  { iFrame. iIntros "QI !>". iSplitL "QI â—ed"; [|by auto].
+  { iFrame. iIntros "QI !>". iSplitL "QI"; [|by auto].
     iNext. iExists _. iFrame. done. }
   iIntros (V' G' enqId enq Venq M') "(QI & #âŠ’V' & #QL' & %F)".
   iDestruct (QueueInv_QueueConsistent with "QI") as "#>%QC'".
@@ -255,7 +255,7 @@ Proof.
     move=> /NoDup_app [?][_] /NoDup_app [?][_]? //. }
 
   iAaccIntro with "QI".
-  { iFrame. iIntros "QI !>". iSplitL "QI â—ed"; [|by auto].
+  { iFrame. iIntros "QI !>". iSplitL "QI"; [|by auto].
     iNext. iExists _. iFrame. done. }
   iIntros (v V' G' enqId deqId enq deq Vdeq M') "(QI & #âŠ’V' & #QL' & %F)".
   set (dV := mkGraphEvent deq Vdeq M') in *.
diff --git a/gpfsl-examples/stack/proof_mp_client_graph.v b/gpfsl-examples/stack/proof_mp_client_graph.v
index f1451e829430f9b6de19c01985ab61cc4938243b..241d041a481a311c435abd8a867c6a6eac9fd5d6 100644
--- a/gpfsl-examples/stack/proof_mp_client_graph.v
+++ b/gpfsl-examples/stack/proof_mp_client_graph.v
@@ -139,7 +139,7 @@ Section Stack.
       iDestruct (graph_master_consistent with "Gm") as %EGC.
       iSpecialize ("SI" with "[$Gm]").
       iAaccIntro with "SI".
-      { iIntros "SI !>". iFrame. iNext. rewrite /StackInv1. iExists G. iFrame. }
+      { iIntros "SI !>". iFrame. }
 
       iIntros (v V' G' pushId popId push1 pop Vpush M') "(SI' & sV' & Local & F)".
       iDestruct "F" as %((SubG' & SubM' & Sub' & Sub'') & CASE).
diff --git a/gpfsl-examples/stack/proof_mp_client_history.v b/gpfsl-examples/stack/proof_mp_client_history.v
index 99ae76260b3cd367d10c892ec21d5873b7ab64c2..79c31967a748b17c1b6e1b6006f04bbd8eef89cc 100644
--- a/gpfsl-examples/stack/proof_mp_client_history.v
+++ b/gpfsl-examples/stack/proof_mp_client_history.v
@@ -137,7 +137,7 @@ Section Stack.
       iDestruct (history_master_wf with "Em") as %EWF.
       iSpecialize ("SI" with "[$Em]").
       iAaccIntro with "SI".
-      { iIntros "SI !>". iFrame. iNext. rewrite /StackInv1. iExists E. iFrame. }
+      { iIntros "SI !>". iFrame. }
 
       iIntros (v V' E' pushId popId push1 pop Vpush M') "(SI' & sV' & Local & F)".
       iDestruct "F" as %((? & ?) & CASE).
diff --git a/gpfsl-examples/stack/proof_treiber_graph.v b/gpfsl-examples/stack/proof_treiber_graph.v
index 314a1cbff8385565557427ef5c62aaf6a4096a83..97a6c29071e8127e99dc8e339183fdb38786a109 100644
--- a/gpfsl-examples/stack/proof_treiber_graph.v
+++ b/gpfsl-examples/stack/proof_treiber_graph.v
@@ -777,7 +777,7 @@ Lemma StackInv_graph_master_acc_instance :
     âˆƒ q', graph_master Î³g q' G âˆ— (graph_master Î³g q' G -âˆ— StackInv Î³g s q G).
 Proof.
   intros. iDestruct 1 as (Î³ T SC) "[? ?]". iExists _. iFrame.
-  iIntros "G". iExists Î³, T. by iFrame.
+  iIntros "G". by iFrame.
 Qed.
 
 Lemma StackInv_graph_snap_instance :
diff --git a/gpfsl/gps/model_rules_init.v b/gpfsl/gps/model_rules_init.v
index 4fd727fbd9e1d1494c4fb20ad91869285cb8eddf..0b90f9561a69568dfbec6d54ca8fde775d502e14 100644
--- a/gpfsl/gps/model_rules_init.v
+++ b/gpfsl/gps/model_rules_init.v
@@ -203,11 +203,11 @@ Section RawRules.
         * by apply SWConnect_singleton. }
     iIntros "!>". rewrite -EqÏ‡. iFrame "oS". destruct bs.
     - iSplitR "W".
-      + iExists Î¼, Î³s, Î³l, Î¶, t. iSplit; [done|]. iNext. by iFrame.
+      + iExists Î¼, Î¶, t. iNext. by iFrame.
       + iExists _. by iFrame.
     - iDestruct (AtomicPtsToX_SW_to_CON_2 with "Pts W") as "[Pts SY]".
       iSplitR "SY".
-      + iExists Î¼, Î³s, Î³l, Î¶, t. iSplit; [done|].
+      + iExists Î¼, Î¶, t.
         iNext. iFrame. iPureIntro. do 2 (split; [done|]).
         by move => ? [?/lookup_singleton_Some [->]].
       + iExists _. by iFrame.
diff --git a/gpfsl/logic/atomic_preds.v b/gpfsl/logic/atomic_preds.v
index d33d36fd3cb35a056457b26287589d3ebe63b732..fa36735ddc3456e3272281468ac626830ddc119b 100644
--- a/gpfsl/logic/atomic_preds.v
+++ b/gpfsl/logic/atomic_preds.v
@@ -1477,7 +1477,7 @@ Proof.
   iIntros "P NA". rewrite AtomicPtsTo_eq.
   iMod (AtomicPtsToX_from_na_cofinite_rel with "P NA")
     as (Î³ t V FR) "(sV & P & W & Pt)".
-  iIntros "!>". iExists Î³, t, V. iFrame (FR) "âˆ—". by iExists _.
+  iIntros "!>". iExists Î³, t, V. iFrame (FR) "âˆ—".
 Qed.
 Lemma AtomicPtsTo_from_na_cofinite l v (G : gset gname) :
   l â†¦ v ==âˆ— âˆƒ Î³ t V, âŒœÎ³ âˆ‰ GâŒ âˆ— âŠ’V âˆ—