diff --git a/theories/flat.v b/theories/flat.v
index 9850ce9c84a74a89a8be630d0ec5509a270503f9..07b98eb41d634721be03e754687addacd90767aa 100644
--- a/theories/flat.v
+++ b/theories/flat.v
@@ -130,13 +130,8 @@ Section proof.
     iFrame. iFrame "#".
   Qed.
 
-  Definition f_spec (R: iProp Σ) (f: val) (Rf: iProp Σ) x :=
-    {{{ inv N R ∗ Rf }}}
-      f x
-    {{{ RET #(); Rf }}}.
-
   Lemma doOp_f_spec R γm γr (p: loc) ts:
-    f_spec (p_inv R γm γr ts p) doOp (own γr (Excl ()) ∗ R)%I #p.
+    f_spec N (p_inv R γm γr ts p) doOp (own γr (Excl ()) ∗ R)%I #p.
   Proof.
     iIntros (Φ) "(#H1 & Hor & HR) HΦ".
     wp_rec. wp_bind (! _)%E.
diff --git a/theories/peritem.v b/theories/peritem.v
index dee70a57a2c377ac64df6349aec99cf3a2fc65be..76a54ad56793035019ee3a43e718cea271954d04 100644
--- a/theories/peritem.v
+++ b/theories/peritem.v
@@ -30,6 +30,12 @@ Section defs.
       iDestruct (IHxs' with "[Hs']") as ">[Hs1 Hs2]"; first by iFrame.
       iModIntro. iSplitL "Hhd Hs1"; iExists hd', (q / 2)%Qp; by iFrame.
   Qed.
+
+  Definition f_spec (R: iProp Σ) (f: val) (Rf: iProp Σ) x :=
+    {{{ inv N R ∗ Rf }}}
+      f x
+    {{{ RET #(); Rf }}}.
+
 End defs.
 
 Section proofs.