diff --git a/gpfsl-examples/queue/proof_spsc_graph.v b/gpfsl-examples/queue/proof_spsc_graph.v
index 5541b28c88c52cbb90d69a1ecb31875437181ce2..bc2de328cb0fe4aa6cb232626c8167c6c61fc563 100644
--- a/gpfsl-examples/queue/proof_spsc_graph.v
+++ b/gpfsl-examples/queue/proof_spsc_graph.v
@@ -157,7 +157,7 @@ Proof.
   iIntros (Φ) "_ Post".
   iMod QE_alloc as (γed) "(●ed & ◯e & ◯d)".
   iApply (wq.(new_queue_spec) with "[%//]").
-  iIntros "!> * [#QL QI]". iApply "Post". unfold SPSCInv.
+  iIntros "!> * [#QL QI]". iApply "Post".
   iFrame "#∗". iPureIntro. split_and!; [done..|].
   exists []. split_and!; [done|done|done| |done..].
   split; [done|]. intros (?&?&?). done.
diff --git a/gpfsl-examples/stack/proof_elim_graph.v b/gpfsl-examples/stack/proof_elim_graph.v
index 1f24d1d6d38e0448d2d7e538864b657cbdb31d4e..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 "?". unfold StackInv'. eauto 10 with iFrame.
+  iExists _. iFrame. by iIntros "?".
 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 a650468b7076683e44e09e235bbccdd46e783963..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 (?????????) "(? & $ & ?)". unfold StackInv. iIntros "$". eauto 11 with iFrame.
+  intros. iDestruct 1 as (?????????) "(? & $ & ?)". iIntros "$". by iFrame.
 Qed.
 
 Lemma StackInv_history_snap_instance :