diff --git a/coq-gpfsl.opam b/coq-gpfsl.opam
index b6210464ebe6245e1ce9c8238b0719a39c1b1efa..041fe5405bb9c0089a3e1bc2053f13e8228bd4f3 100644
--- a/coq-gpfsl.opam
+++ b/coq-gpfsl.opam
@@ -10,7 +10,7 @@ version: "dev"
 synopsis: "A combination of GPS and FSL in the promising semantics WITHOUT promises"
 
 depends: [
-  "coq-iris"  { (= "dev.2024-02-06.0.66d2e339") | (= "dev") }
+  "coq-iris"  { (= "dev.2024-02-16.1.06f499e0") | (= "dev") }
   "coq-orc11" {= version}
 ]
 
diff --git a/coq-orc11.opam b/coq-orc11.opam
index 1b31f393d6261dacf7d03f44016a9882de4a7765..d0b0a081e059693bd1308d0f5439644c65a866df 100644
--- a/coq-orc11.opam
+++ b/coq-orc11.opam
@@ -10,7 +10,7 @@ version: "dev"
 synopsis: "A Coq formalization of the ORC11 semantics for weak memory"
 
 depends: [
-  "coq-stdpp" { (= "dev.2024-02-02.1.a2456618") | (= "dev") }
+  "coq-stdpp" { (= "dev.2024-02-09.0.cafd7113") | (= "dev") }
 ]
 
 build: ["./make-package" "orc11" "-j%{jobs}%"]
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/exchanger/proof_mp_client.v b/gpfsl-examples/exchanger/proof_mp_client.v
index 155926b6a6c3a51e0e66d585a82542275ce09fea..726ee011ad50cefca92afc521f57e5da9382c388 100644
--- a/gpfsl-examples/exchanger/proof_mp_client.v
+++ b/gpfsl-examples/exchanger/proof_mp_client.v
@@ -79,8 +79,7 @@ Section ex.
     iMod (own_alloc (●E false ⋅ ◯E false)) as (γ2) "[Tokγ22 Tokγ21]";
       [apply excl_auth_valid|].
     iMod (inv_alloc N' _ (ExInv γg γ1 γ2) with "[Hex Tokγ12 Tokγ22]") as "#II".
-    { iNext; iExists ∅; iFrame.
-      iExists false, false. rewrite /list_max_2 /=. by iFrame. }
+    { iNext; iExists ∅; iFrame. rewrite /list_max_2 //=. }
 
     iDestruct (view_at_intro True%I with "[//]") as (V0) "[#sV0 _]".
     wp_apply (wp_fork with "[Tokγ11]"); [done|..].
@@ -198,7 +197,7 @@ Section ex.
       iMod "Hclose" as "_".
       iDestruct "Hown" as (b1' b2') "[Hown >[%Hsize %Eqb1]]".
       iMod ("Close" with "[Hown EI]") as "_".
-      { iNext. iExists G2'. iFrame. iExists b1', b2'. by iFrame. }
+      { iNext. iExists G2'. iFrame. done. }
 
       iIntros "!>". iApply "Post". iPureIntro.
 
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 ddb84f161c7a3ae938e0837b6c0d6eb2e4267370..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".
@@ -1361,7 +1361,7 @@ Lemma QueueInv_no_exist_QueueLocs_access γg q Q G γ γh γl η s D L T :
 Proof.
   iIntros (E) "(LEL & LD & LT & F & QV & QL)".
   iDestruct "QL" as (Vb) "QL".
-  iExists Vb. iFrame "QL". iIntros (Vb') "QL". iFrame. by iExists Vb'.
+  iExists Vb. iFrame "QL". iIntros (Vb') "QL". iFrame.
 Qed.
 
 Lemma QueueInv_no_exist_tail_access γg q Q G γ γh γl η s D L T :
@@ -1391,7 +1391,7 @@ Lemma QueueInv_no_exist_tail_immut_access γg q Q G γ γh γl η s D L T :
 Proof.
   intros E. rewrite ->QueueInv_no_exist_tail_access.
   iDestruct 1 as (Vb ζl) "[[T #Tls] Close]".
-  iExists Vb, ζl. iFrame "T Tls".
+  iExists Vb, ζl. iFrame "T". iSplitR; [iFrame "#" | ].
   iIntros (Vb') "T". iApply ("Close" $! (Vb' ⊔ Vb)). by iFrame "#∗".
 Qed.
 
@@ -1406,8 +1406,8 @@ Proof.
   intros DL E. rewrite ->QueueInv_no_exist_QueueLocs_access.
   iDestruct 1 as (Vb) "[[H TNs] Close]".
   iDestruct "H" as (t0 Vs) "[H #Hs]".
-  iExists Vb, t0, Vs. iFrame "#∗". iIntros (Vb') "H".
-  iApply ("Close" $! (Vb' ⊔ Vb)). iFrame. iExists t0, Vs. by iFrame "#∗".
+  iExists Vb, t0, Vs. iFrame "H". iSplitR; [iFrame "Hs" | ]. iIntros (Vb') "H".
+  iApply ("Close" $! (Vb' ⊔ Vb)). iFrame "#∗".
 Qed.
 
 Lemma QueueInv_agree γg q Q G Q' G' :
diff --git a/gpfsl-examples/queue/proof_spsc_graph.v b/gpfsl-examples/queue/proof_spsc_graph.v
index 2afaa935a0d38766b922aadc8ab3166bb5d72120..bc2de328cb0fe4aa6cb232626c8167c6c61fc563 100644
--- a/gpfsl-examples/queue/proof_spsc_graph.v
+++ b/gpfsl-examples/queue/proof_spsc_graph.v
@@ -181,7 +181,7 @@ Proof.
 
   iAaccIntro with "QI".
   { iFrame. iIntros "QI !>". iSplitL "QI"; [|by auto].
-    iNext. iExists _. iFrame "QI". done. }
+    iNext. iExists _. iFrame. done. }
   iIntros (V' G' enqId enq Venq M') "(QI & #⊒V' & #QL' & %F)".
   iDestruct (QueueInv_QueueConsistent with "QI") as "#>%QC'".
   rewrite /is_enqueue in F.
@@ -256,7 +256,7 @@ Proof.
 
   iAaccIntro with "QI".
   { iFrame. iIntros "QI !>". iSplitL "QI"; [|by auto].
-    iNext. iExists _. iFrame "QI". done. }
+    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 *.
   iDestruct (QueueInv_QueueConsistent with "QI") as "#>%QC'".
diff --git a/gpfsl-examples/stack/proof_elim_graph.v b/gpfsl-examples/stack/proof_elim_graph.v
index dc940919d3976d143db37ae44e8defdc14f3c767..366cd6dc22cbf1142c1e17a6154ffda374b0dd83 100644
--- a/gpfsl-examples/stack/proof_elim_graph.v
+++ b/gpfsl-examples/stack/proof_elim_graph.v
@@ -749,7 +749,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 (?????????) "[(?&?&?) ?]".
-  iExists _. iFrame. iIntros "?". eauto 10 with iFrame.
+  iExists _. iFrame. by iIntros "?".
 Qed.
 
 Lemma StackInv'_graph_snap_instance :
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_at.v b/gpfsl-examples/stack/proof_treiber_at.v
index 3090bebc4584bb3a4ca75626a68cc7c6d43d86df..8ce8dede4bc41ee7e3e437cbbc8bac2e8c06bc66 100644
--- a/gpfsl-examples/stack/proof_treiber_at.v
+++ b/gpfsl-examples/stack/proof_treiber_at.v
@@ -366,7 +366,7 @@ Proof.
       rewrite /all_slocs /=. iSplitL; [|done]. iExists _, (hd_error S2).
       iFrame "Hn1".
     - rewrite in_sloc_cons. iFrame "Is".
-      iExists v. rewrite /= /in_sloc. iFrame. iExists _. by iFrame "Hn2". }
+      iExists v. rewrite /= /in_sloc. by iFrame. }
 
   (* re-establish the invariant *)
   iMod ("Close" with "[-Post Hmn]") as "_".
diff --git a/gpfsl-examples/stack/proof_treiber_graph.v b/gpfsl-examples/stack/proof_treiber_graph.v
index e214c7024401a65c75f72c30bd2683e45309fbcb..97a6c29071e8127e99dc8e339183fdb38786a109 100644
--- a/gpfsl-examples/stack/proof_treiber_graph.v
+++ b/gpfsl-examples/stack/proof_treiber_graph.v
@@ -602,7 +602,7 @@ Lemma StackInv_no_exist_StackLocs_access s G γ γh T S :
       ∗ (∀ Vb, @{Vb} StackLocs s G.(Es) γh T S -∗ StackInv_no_exist s G γ γh T S).
 Proof.
   iIntros "(F & SV & SL)". iDestruct "SL" as (Vb) "SL".
-  iExists Vb. iFrame "SL". iIntros (Vb') "SL". iFrame. by iExists Vb'.
+  iExists Vb. iFrame "SL". iIntros (Vb') "SL". iFrame.
 Qed.
 
 Lemma StackLocs_no_exist_head_immut_access s E γh T S t0 LVs Vh :
@@ -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-examples/stack/proof_treiber_history.v b/gpfsl-examples/stack/proof_treiber_history.v
index 3fe11fb6f8c9469482e95fb78ba8f5c58b045804..a473366f4f6d597ee4ea172e39492dfa6f43cb0d 100644
--- a/gpfsl-examples/stack/proof_treiber_history.v
+++ b/gpfsl-examples/stack/proof_treiber_history.v
@@ -1432,7 +1432,7 @@ Lemma StackInv_history_master_acc_instance :
     history_master γg 1 E ∗
     (history_master γg 1 E -∗ StackInv γg s E).
 Proof.
-  intros. iDestruct 1 as (?????????) "(? & $ & ?)". iIntros "$". eauto 11 with iFrame.
+  intros. iDestruct 1 as (?????????) "(? & $ & ?)". iIntros "$". by iFrame.
 Qed.
 
 Lemma StackInv_history_snap_instance :
@@ -2003,7 +2003,7 @@ Proof.
 
       iSplitL.
       + iExists _,_,_. iExists esi1',emo1,stk1',ont1,Vt1,Vi1.
-        iFrame "∗". iSplitL; last iSplitL; first by eauto with iFrame.
+        iFrame "∗". iSplitL.
         { (* SeenMsgsAll γh s E1' esi1' emo1 ti. *)
           iNext. iIntros (e eidx eV EV EMO_LOOKUP).
           case (decide (eidx = emo_e O (length esi1))) as [->|NEeidx].
@@ -2113,7 +2113,7 @@ Proof.
       iSplitL.
       + iExists _,_,_. iExists esi1,emo1',stk1',ont1,Vt1,Vi1.
         rewrite (_ : emo1.*2 = emo1'.*2); last by rewrite emo_insert_e_2.
-        iFrame "∗". iSplitL; last iSplitL; first by eauto with iFrame.
+        iFrame "∗". iSplitL.
         { (* SeenMsgsAll γh s E1' esi1 emo1' ti *)
           iNext. iIntros (e eidx eV EV EMO_LOOKUP).
           case (decide (eidx = emo_e (S gen') (length es))) as [->|NEeidx].
diff --git a/gpfsl/base_logic/frame_instances.v b/gpfsl/base_logic/frame_instances.v
index 0a633d2f19449f64fc6bbf76bad20a96e28e1cca..ef7bf57f27cbf305d1f4b847458635bedcd88551 100644
--- a/gpfsl/base_logic/frame_instances.v
+++ b/gpfsl/base_logic/frame_instances.v
@@ -102,10 +102,11 @@ Proof.
 Qed.
 
 #[global] Instance frame_view_at_view_mono p R P Q V1 V2 :
-  IsBiIndexRel V1 V2 →
+  TCNoBackTrack (IsBiIndexRel V1 V2) → 
+  (* [IsBiIndexRel] can loop if V2 is an evar, due to the [lat_meet_glb] hint *)
   Frame p R P Q → Frame p (@{V1} R) (@{V2} P) (@{V2} Q).
 Proof.
-  rewrite /Frame /IsBiIndexRel -view_at_intuitionistically_if => -> H.
+  rewrite /Frame /IsBiIndexRel -view_at_intuitionistically_if => [[->]] H.
   rewrite -view_at_sep.
   by apply bi.wand_entails, view_at_wand_2, view_at_at, bi.entails_wand.
 Qed.
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_ops.v b/gpfsl/logic/atomic_ops.v
index 1915b7b54e0f93c91f24d8981a83d31e389680dc..da165976a0bc6addf4293701dacdeb2fe2ff67c0 100644
--- a/gpfsl/logic/atomic_ops.v
+++ b/gpfsl/logic/atomic_ops.v
@@ -591,8 +591,7 @@ Proof.
   iApply (AtomicSeen_write _ _ _ _ _ q tx' with "[$SS $Pts SE $sV $HV]");
     [done..|].
   iIntros "!>" (t' V' V'') "(F & sV'' & SN' & SE & SY & Pts)".
-  iApply ("Post" $! t' V' V''). iFrame.
-  iExists tx'. iFrame "SE". iPureIntro.
+  iApply ("Post" $! t' V' V''). iFrame. iPureIntro.
   case (decide (tx' = t')) => [->|?].
   - rewrite lookup_insert. by eexists.
   - by rewrite lookup_insert_ne.
@@ -1519,7 +1518,7 @@ Proof.
   iApply (AtomicSeen_CAS with "[$S $P $sV $HRel Pr]"); [done..|].
   iIntros "!>" (b t' v' Vr V'' ζ'' ζn) "(F & sV'' & S' & P & Pr & CASE)".
   iApply "Post". iFrame.
-  rewrite AtomicPtsTo_CON_CAS. iFrame. iExists _. by iFrame.
+  rewrite AtomicPtsTo_CON_CAS. iFrame. done.
 Qed.
 
 Lemma AtomicSeen_CON_CAS_int
diff --git a/gpfsl/logic/atomic_ops_vj.v b/gpfsl/logic/atomic_ops_vj.v
index ebb0c5a42859afd809a0ff83d014c39e660d3145..ec128f47029933dc2e9a233bfe4079a0d857c4a9 100644
--- a/gpfsl/logic/atomic_ops_vj.v
+++ b/gpfsl/logic/atomic_ops_vj.v
@@ -208,8 +208,7 @@ Proof.
   iApply (AtomicSeen_write_vj _ _ _ _ _ q tx' with "[$SS $Pts SE $sV $HV]");
     [done..|].
   iIntros "!>" (t' V' V'') "(F & sV'' & SN' & SE & SY & Pts)".
-  iApply ("Post" $! t' V' V''). iFrame.
-  iExists tx'. iFrame "SE". iPureIntro.
+  iApply ("Post" $! t' V' V''). iFrame. iPureIntro.
   case (decide (tx' = t')) => [->|?].
   - rewrite lookup_insert. by eexists.
   - by rewrite lookup_insert_ne.
diff --git a/gpfsl/logic/atomic_preds.v b/gpfsl/logic/atomic_preds.v
index 638f1b4da998c8d953fcb9729167ca185c3d4440..fa36735ddc3456e3272281468ac626830ddc119b 100644
--- a/gpfsl/logic/atomic_preds.v
+++ b/gpfsl/logic/atomic_preds.v
@@ -1278,7 +1278,7 @@ Proof.
   intros C GH VAL.
   iIntros "(? & sVm & ? & ? & NAL & HC & AR & AW & NA)".
   iExists t, m. iFrame (VAL) "sVm".
-  iExists rsa, rsn, ws. iFrame (GH) "∗". iSplitR "NAL"; last by eauto.
+  iExists rsa, rsn, ws. iFrame (GH) "∗".
   iStopProof. constructor => V. iPureIntro. intros ?.
   exists t, m. split; last split; [by rewrite lookup_singleton|by inversion VAL|done].
 Qed.
@@ -1404,7 +1404,7 @@ Proof.
       * apply map_non_empty_singleton.
       * exists {[t := m]}. split; [done|].
         move => ?? /lookup_singleton_Some [? <-]. by inversion VAL.
-    + iExists t. iFrame. iPureIntro. rewrite Eqζ. split.
+    + iPureIntro. rewrite Eqζ. split.
       * rewrite lookup_insert. by eexists.
       * move => t1 [VV1 /lookup_singleton_Some [<-//]].
   - iExists {[t := m]}, Va, rsa, rsn, ws. iFrame "SA". iFrame "#∗".
@@ -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 ∗
diff --git a/gpfsl/logic/readonly_ptsto.v b/gpfsl/logic/readonly_ptsto.v
index af767f91396ceb5a7c16dec7c29f8cfba306aea7..007c9221538ad4f93f4de3e41d9043909f2bf094 100644
--- a/gpfsl/logic/readonly_ptsto.v
+++ b/gpfsl/logic/readonly_ptsto.v
@@ -260,8 +260,7 @@ Proof.
   iSplitL; last first. { by iApply (monPred_in_mono with "sV'"). }
   iDestruct (view_at_elim with "sV' AWL") as "AWL".
   iExists rsa, rns, ws. iFrame (GH) "∗".
-  iDestruct (seen_time_AllocLocal_singleton with "st") as "$"; [by inversion Eqv'|].
-  eauto.
+  iDestruct (seen_time_AllocLocal_singleton with "st") as "$". by inversion Eqv'.
 Qed.
 
 End ops_rules.