diff --git a/gpfsl-examples/stack/proof_elim_graph.v b/gpfsl-examples/stack/proof_elim_graph.v
index 366cd6dc22cbf1142c1e17a6154ffda374b0dd83..5c0c3ec4b80bb06149687695c49d3d40a7fbccbb 100644
--- a/gpfsl-examples/stack/proof_elim_graph.v
+++ b/gpfsl-examples/stack/proof_elim_graph.v
@@ -748,8 +748,8 @@ Lemma StackInv'_graph_master_acc_instance :
   ∀ γg s q G, StackInv' γg s q G ⊢
     ∃ q', graph_master γg q' G ∗ (graph_master γg q' G -∗ StackInv' γg s q G).
 Proof.
-  intros. iDestruct 1 as (?????????) "[(?&?&?) ?]".
-  iExists _. iFrame. by iIntros "?".
+  intros. iDestruct 1 as (?????????) "[(?&$&?) ?]".
+  iIntros "$". by iFrame.
 Qed.
 
 Lemma StackInv'_graph_snap_instance :