diff --git a/flat.v b/flat.v
index 3753263de335ad1608eab69578f97efc61b79986..3906ebea5d695e73e9a4d47a4fcdd909fa8124a2 100644
--- a/flat.v
+++ b/flat.v
@@ -183,116 +183,111 @@ Section proof.
     ⊢ WP iter #hd doOp {{ Φ }}.
   Proof.
     iIntros (HN) "(#Hf & #? & Ho2 & HR & Hlist' & HΦ)".
-    iApply pvs_wp.
-    iDestruct (dup_is_list' with "[Hlist']") as "==>[Hl1 Hl2]"; first by iFrame.
-    iDestruct (dup_is_list' with "[Hl2]") as "==>[Hl2 Hl3]"; first by iFrame.
-    iVsIntro.
-    iDestruct (iter_spec _ (p_inv R γm γr) (fun v => v = #() ★ own γr (Excl ()) ★ R)%I γs s
-                         (is_list' γs hd xs ★ own γr (Excl ()) ★ R)%I (srv_tokm_inv γm) xs hd
-                         doOp doOp
-                         with "[-Hl1 HΦ]") as "Hiter"=>//.
+    iApply (iter_spec N (p_inv R γm γr) Φ
+                      (* (fun v => v = #() ★ own γr (Excl ()) ★ R)%I *)
+                      γs s (own γr (Excl ()) ★ R)%I (srv_tokm_inv γm) xs hd doOp doOp
+            with "[-]")=>//.
     - rewrite /f_spec.
-      iIntros (Φ' p _ Hin) "(#Hh & #? & (Hls & Ho2 & HR) & HΦ')".
-      wp_let. wp_bind (! _)%E. iInv N as "[Hs >Hm]" "Hclose".
-      iDestruct "Hs" as (xs' hd') "[>Hhd [>Hxs HRs]]".
-      iDestruct (dup_is_list' with "[Hls]") as "==>[Hls1 Hls2]"; first by iFrame.
+      iIntros (Φ' x _) "(#Hh & #? & Hev & [Hor HR] & HΦ')".
+      iDestruct "Hev" as (xhd) "#Hev".
+      wp_rec.  wp_bind (! _)%E. iInv N as "[Hs >Hm]" "Hclose".
+      iDestruct "Hs" as (gxs ghd) "[>Hghd [>Hgxs HRs]]". (* global xs, hd *)
       iDestruct "HRs" as (m) "[>Hom HRs]".
       (* acccess *)
-      iDestruct (access with "[Hom HRs Hls1]") as (hd'') "(Hrest & HRx & % & Hom)"=>//; first iFrame.
-      iDestruct "HRx" as (v') "[>% [Hpinv' >Hhd'']]". inversion H0. subst.
+      iDestruct (ev_map_witness _ _ _ m with "[Hev Hom]") as %H'; first by iFrame.
+      iDestruct (big_sepM_delete_later (perR _) m with "HRs") as "[Hp HRm]"=>//.
+      iDestruct "Hp" as (v') "[>% [Hpinv' >Hahd]]". inversion H. subst.
       iDestruct "Hpinv'" as (ts p'') "[>% [>#Hevm [Hp | [Hp | [Hp | Hp]]]]]"; subst.
       + iDestruct "Hp" as (y) "(>Hp & Hs)".
-        wp_load. iVs ("Hclose" with "[-HΦ' Ho2 HR Hls2]").
-        { iNext. iFrame. iExists xs', hd'.
-          iFrame "Hhd Hxs". iExists m.
-          iFrame "Hom". iDestruct (big_sepM_delete _ m with "[Hrest Hhd'' Hevm Hp Hs]") as "?"=>//.
+        wp_load. iVs ("Hclose" with "[-Hor HR Hev HΦ']").
+        { iNext. iFrame. iExists gxs, ghd.
+          iFrame "Hghd Hgxs". iExists m.
+          iFrame "Hom". iDestruct (big_sepM_delete _ m with "[-]") as "?"=>//.
           iFrame. iExists #p''. iSplitR; first done. iExists ts, p''.
           iSplitR; first done. iFrame "#". iLeft. iExists y. iFrame. }
-        iVsIntro. wp_match. iApply "HΦ'". by iFrame.
+        iVsIntro. wp_match. iVsIntro. iApply ("HΦ'" with "[Hor HR]"). iFrame.
       + iDestruct "Hp" as (f' x') "(Hp & Hs)".
         wp_load. destruct ts as [[[[γx γ1] γ3] γ4] γq].
-        iDestruct "Hs" as (P Q) "(Hx & Hpx & Hf & HoQ& Ho1 & Ho4)".
+        iDestruct "Hs" as (P Q) "(Hx & Hpx & Hf' & HoQ & Ho1 & Ho4)".
         iAssert (|=r=> own γx (((1/2/2)%Qp, DecAgree x') ⋅
                                ((1/2/2)%Qp, DecAgree x')))%I with "[Hx]" as "==>[Hx1 Hx2]".
         { iDestruct (own_update with "Hx") as "?"; last by iAssumption.
           rewrite -{1}(Qp_div_2 (1/2)%Qp).
           by apply pair_l_frac_op'. }
-        iVs ("Hclose" with "[-Hf Hls2 Ho1 Hx2 HR HoQ Hpx HΦ']").
-        { iNext. iFrame. iExists xs', hd'.
-          iFrame "Hhd Hxs". iExists m.
+        iVs ("Hclose" with "[-Hf' Ho1 Hx2 HR HoQ HΦ' Hpx]").
+        { iNext. iFrame. iExists gxs, ghd.
+          iFrame "Hghd Hgxs". iExists m.
           iFrame "Hom". iDestruct (big_sepM_delete _ m with "[-]") as "?"=>//.
           simpl. iFrame. iExists #p''. iSplitR; auto. rewrite /allocated.
           iExists (γx, γ1, γ3, γ4, γq), p''. iSplitR; auto.
           iFrame "#". iRight. iRight. iLeft. iExists f', x'. iFrame. }
         iVsIntro. wp_match.
         wp_proj. wp_proj.
-        wp_bind (f' _). iApply wp_wand_r. iSplitL "Hpx Hf HR".
-        { iApply "Hf". iFrame. }
+        wp_bind (f' _). iApply wp_wand_r. iSplitL "Hpx Hf' HR".
+        { iApply "Hf'". iFrame. }
         iIntros (v) "[HR HQ]".
         wp_value. iVsIntro. iInv N as "[Hs >Hm]" "Hclose".
         iDestruct "Hs" as (xs'' hd''') "[>Hhd [>Hxs HRs]]".
         iDestruct "HRs" as (m') "[>Hom HRs]".
-        iDestruct (dup_is_list' with "[Hls2]") as "==>[Hls2 Hls3]"; first by iFrame.
-        iDestruct (access with "[Hom HRs Hls2]") as (hd'''') "(Hrest & HRx & % & Hom)"=>//; first iFrame.
-        iDestruct "HRx" as (v'') "[>% [Hpinv' >Hhd'']]". inversion H2. subst.
+        iDestruct (ev_map_witness _ _ _ m' with "[Hevm Hom]") as %?; first by iFrame.
+        iDestruct (big_sepM_delete_later (perR _) m' with "HRs") as "[Hp HRm]"=>//.
+        iDestruct "Hp" as (v'') "[>% [Hpinv' >Hhd'']]". inversion H1. subst.
         iDestruct "Hpinv'" as ([[[[γx' γ1'] γ3'] γ4'] γq'] p'''') "[>% [>#Hevm2 Hps]]".
-        inversion H3. subst.
-        destruct (decide (γ1 = γ1' ∧ γx = γx' ∧ γ3 = γ3' ∧ γ4 = γ4' ∧ γq = γq')) as [[? [? [? [? ?]]]]|Hneq]; subst.
+        inversion H2. subst.
+        destruct (decide (γ1 = γ1' ∧ γx = γx' ∧ γ3 = γ3' ∧ γ4 = γ4' ∧ γq = γq'))
+          as [[? [? [? [? ?]]]]|Hneq]; subst.
         {
           iDestruct "Hps" as "[Hp | [Hp | [Hp | Hp]]]".
           * iDestruct "Hp" as (?) "(_ & >Ho1' & _)".
             iApply excl_falso. iFrame.
           * iDestruct "Hp" as (? ?) "[>? Hs]". iDestruct "Hs" as (? ?) "(_ & _ & _ & _ & >Ho1' & _)".
             iApply excl_falso. iFrame.
-          * iDestruct "Hp" as (? x5) ">(Hp & Hx & Ho2 & Ho4)".
-            iDestruct "Hm" as (m2) "[Hom2 HRm]".
-            destruct (m2 !! p'''') eqn:Heqn.
-            {
-              iDestruct (big_sepM_delete _ m2 with "HRm") as "[HRk HRm]"=>//.
-              iDestruct "HRk" as (?) "HRk".
-              iDestruct (heap_mapsto_op_1 with "[HRk Hp]") as "[% Hp]"; first by iFrame.
-              rewrite Qp_div_2. wp_store.
-              (* now close the invariant *)
-              iDestruct (m_frag_agree' with "[Hx Hx2]") as "[Hx %]"; first iFrame.
-              subst. rewrite Qp_div_2. iVs ("Hclose" with "[-HΦ' Ho2 HR Hls3]").
-              { iNext. iDestruct "Hp" as "[Hp1 Hp2]".
-                iAssert (srv_tokm_inv γm) with "[Hp1 HRm Hom2]" as "HRm".
-                { iExists m2. iFrame. iApply (big_sepM_delete _ m2)=>//.
-                  iFrame. eauto. }
-                iFrame. iExists xs''. iFrame. iExists hd'''. iFrame.
-                iExists m'. iFrame.
-                iDestruct (big_sepM_delete _ m' with "[-]") as "?"=>//.
-                { simpl. iFrame. iExists #p''''.
-                  iSplitR; first auto. iExists (γx', γ1', γ3', γ4', γq'), p''''.
-                  iSplitR; first auto. iFrame "Hevm". iRight. iRight.
-                  iRight. iExists x5, v. iFrame.
-                  iExists Q. iFrame.                  
-                }
+          * iDestruct "Hp" as (? x5) ">(Hp & Hx & Hor & Ho4)".
+            iDestruct "Hm" as (m2) "[Hom2 HRp]".
+            iDestruct (ev_map_witness _ _ _ m2 with "[Hevm Hom2]") as %?; first by iFrame.
+            iDestruct (big_sepM_delete _ m2 with "HRp") as "[HRk HRp]"=>//.
+            iDestruct "HRk" as (?) "HRk".
+            iDestruct (heap_mapsto_op_1 with "[HRk Hp]") as "[% Hp]"; first by iFrame.
+            rewrite Qp_div_2. wp_store.
+            (* now close the invariant *)
+            iDestruct (m_frag_agree' with "[Hx Hx2]") as "[Hx %]"; first iFrame.
+            subst. rewrite Qp_div_2. iVs ("Hclose" with "[-HR Hor HΦ']").
+            { iNext. iDestruct "Hp" as "[Hp1 Hp2]".
+              iAssert (srv_tokm_inv γm) with "[Hp1 HRp Hom2]" as "HRp".
+              { iExists m2. iFrame. iApply (big_sepM_delete _ m2)=>//.
+                iFrame. eauto. }
+              iFrame. iExists xs''. iFrame. iExists hd'''. iFrame.
+              iExists m'. iFrame.
+              iDestruct (big_sepM_delete _ m' with "[-]") as "?"=>//.
+              { simpl. iFrame. iExists #p''''.
+                iSplitR; first auto. iExists (γx', γ1', γ3', γ4', γq'), p''''.
+                iSplitR; first auto. iFrame "Hevm". iRight. iRight.
+                iRight. iExists x5, v. iFrame.
+                iExists Q. iFrame. 
               }
-              iApply "HΦ'". by iFrame.
             }
-            { iExFalso. iApply (map_agree_none' _ _ _ m2)=>//. by iFrame. }
+            iApply "HΦ'". iFrame.
           * iDestruct "Hp" as (? ?) "[? Hs]". iDestruct "Hs" as (?) "(_ & _ & _ & >Ho1' & _)".
             iApply excl_falso. iFrame.
         }
         { iDestruct (evmap_frag_agree_split with "[]") as "%"; first iFrame "Hevm Hevm2".
-          inversion H4. subst. by contradiction Hneq. }
+          inversion H3. subst. by contradiction Hneq. }
       + destruct ts as [[[[γx γ1] γ3] γ4] γq]. iDestruct "Hp" as (? x) "(_ & _ & >Ho2' & _)".
         iApply excl_falso. iFrame.
       + destruct ts as [[[[γx γ1] γ3] γ4] γq]. iDestruct "Hp" as (x' y) "[Hp Hs]".
         iDestruct "Hs" as (Q) "(>Hx & HoQ & HQxy & >Ho1 & >Ho4)".
-        wp_load. iVs ("Hclose" with "[-HΦ' HR Ho2 Hls2]").
-        { iNext. iFrame. iExists xs', hd'.
-          iFrame "Hhd Hxs". iExists m.
+        wp_load. iVs ("Hclose" with "[-HΦ' HR Hor]").
+        { iNext. iFrame. iExists gxs, ghd.
+          iFrame "Hghd Hgxs". iExists m.
           iFrame "Hom". iDestruct (big_sepM_delete _ m with "[-]") as "?"=>//.
           iFrame. iExists #p''. iSplitR; first auto. iExists (γx, γ1, γ3, γ4, γq), p''.
           iSplitR; auto. iFrame "#". iRight. iRight. iRight. iExists x', y. iFrame.
           iExists Q. iFrame. }
-        iVsIntro. wp_match. iApply "HΦ'". by iFrame.
+        iVsIntro. wp_match.
+        iApply "HΦ'". iFrame.
     - apply to_of_val.
-    - rewrite /srv_stack_inv. iFrame "#". iFrame. iIntros "(? & ? & ?)". by iFrame.
-    - iApply wp_wand_r. iSplitL "Hiter"; first done.
-      iIntros (?) "[% [Ho2 HR]]". subst. iApply ("HΦ" with "Ho2 HR").
+    - iFrame "#". iFrame. iIntros "[Hor HR]".
+      iApply ("HΦ" with "Hor HR").
   Qed.
 
   Definition own_γ3 (ts: toks) := let '(_, _, γ3, _, _) := ts in own γ3 (Excl ()).
diff --git a/peritem.v b/peritem.v
index c974d2d919a354a48395540e587e32e937b5d4a7..4c6e12924f876700d571a0999f3e8b24561bef8d 100644
--- a/peritem.v
+++ b/peritem.v
@@ -73,12 +73,12 @@ Section defs.
       iVsIntro. iSplitL "Hhd Hs1 Hev"; iExists hd', (q / 2)%Qp; by iFrame.
   Qed.
 
-  Definition f_spec γ (xs: list val) (s hd: loc) (f: val) (Rf RI: iProp Σ) :=
-    (* Rf, RI are some frames *)
+  Definition f_spec γ (xs: list val) (s: loc) (f: val) (Rf RI: iProp Σ) :=
+    (* Rf, RI is some frame *)
     ∀ Φ (x: val),
-      heapN ⊥ N → x ∈ xs →
-      heap_ctx ★ inv N ((∃ xs, is_stack' γ xs s) ★ RI) ★
-      (is_list' γ hd xs ★ Rf) ★ (is_list' γ hd xs -★ Rf -★ Φ #())
+      heapN ⊥ N →
+      heap_ctx ★ inv N ((∃ xs, is_stack' γ xs s) ★ RI) ★ (∃ hd, evs γ hd x) ★
+      Rf ★ (Rf -★ Φ #())
       ⊢ WP f x {{ Φ }}.
 End defs.
 
@@ -106,7 +106,7 @@ Lemma new_stack_spec' Φ RI:
     
   Lemma iter_spec Φ γ s (Rf RI: iProp Σ):
     ∀ xs hd (f: expr) (f': val),
-      heapN ⊥ N → f_spec N R γ xs s hd f' Rf RI → to_val f = Some f' →
+      heapN ⊥ N → f_spec N R γ xs s f' Rf RI → to_val f = Some f' →
       heap_ctx ★ inv N ((∃ xs, is_stack' R γ xs s) ★ RI) ★
       is_list' γ hd xs ★ Rf ★ (Rf -★ Φ #())
       ⊢ WP (iter #hd) f {{ v, Φ v }}.
@@ -116,19 +116,11 @@ Lemma new_stack_spec' Φ RI:
       iDestruct "Hxs1" as (q) "Hhd".
       wp_rec. wp_value. iVsIntro. wp_let. wp_load. wp_match. by iApply "HΦ".
     - simpl. iIntros (hd f f' HN Hf ?) "(#Hh & #? & Hxs1 & HRf & HΦ)".
-      iDestruct "Hxs1" as (hd2 q) "(Hhd & #Hev & Hhd2)".
+      iDestruct "Hxs1" as (hd2 q) "(Hhd & Hev & Hhd2)".
       wp_rec. wp_value. iVsIntro. wp_let. wp_load. wp_match. wp_proj.
-      wp_bind (f' _). iApply Hf=>//; first set_solver.
-      iFrame "#". simpl.
-      iSplitL "Hev Hhd Hhd2 HRf".
-      { iFrame. iExists hd2, q. iFrame. }
-      iIntros "Hls HRf".
+      wp_bind (f' _). iApply Hf=>//. iFrame "#".
+      iSplitL "Hev"; first eauto. iFrame. iIntros "HRf".
       wp_seq. wp_proj. iApply (IHxs' with "[-]")=>//.
-      + rewrite /f_spec. iIntros (? ? ? ?) "(#? & #? & ? & ?)".
-        iApply Hf=>//.
-        * set_solver.
-        * iFrame "#".
-            by iFrame.
       + apply to_of_val.
       + iFrame "#". by iFrame.
   Qed.
@@ -191,30 +183,4 @@ Lemma new_stack_spec' Φ RI:
         by iApply "HΦ".
   Qed.
 
-  (* some helpers *)
-  Lemma access (γ: gname) (x: val) (xs: list val) (m: evmapR loc val unitR) :
-    ∀ hd: loc,
-    x ∈ xs  →
-    ▷ ([★ map] hd↦v ∈ m, perR R hd v) ★ own γ (● m) ★
-    is_list' γ hd xs
-    ⊢ ∃ hd', ▷ ([★ map] hd↦v ∈ delete hd' m, perR R hd v) ★
-             ▷ perR R hd' ((∅: unitR), DecAgree x) ★ m !! hd' = Some ((∅: unitR), DecAgree x) ★ own γ (● m).
-  Proof.
-    induction xs as [|x' xs' IHxs'].
-    - iIntros (? Habsurd). inversion Habsurd.
-    - destruct (decide (x = x')) as [->|Hneq].
-      + iIntros (hd _) "(HR & Hom & Hxs)".
-        simpl. iDestruct "Hxs" as (hd' q) "[Hhd [#Hev Hxs']]".
-        rewrite /evs.
-        iDestruct (ev_map_witness _ _ _ m with "[Hev Hom]") as %H'; first by iFrame.
-        iDestruct (big_sepM_delete_later (perR R) m with "HR") as "[Hp HRm]"=>//.
-        iExists hd. by iFrame.
-      + iIntros (hd ?).
-        assert (x ∈ xs'); first set_solver.
-        iIntros "(HRs & Hom & Hxs')".
-        simpl. iDestruct "Hxs'" as (hd' q) "[Hhd [Hev Hxs']]".
-        iDestruct (IHxs' hd' with "[HRs Hxs' Hom]") as "?"=>//.
-        iFrame.
-  Qed.
-
 End proofs.