diff --git a/iris_heap_lang/lib/counter.v b/iris_heap_lang/lib/counter.v
index a40c90c2b0f554873b3796e74fd9a235155461b1..6efb2e24158b999832ad2d8c827ab9a4dc0704a2 100644
--- a/iris_heap_lang/lib/counter.v
+++ b/iris_heap_lang/lib/counter.v
@@ -35,7 +35,7 @@ Section mono_proof.
   Lemma newcounter_mono_spec :
     {{{ True }}} newcounter #() {{{ l, RET #l; mcounter l 0 }}}.
   Proof.
-    iIntros (Φ) "_ HΦ". rewrite -wp_fupd /newcounter /=. wp_lam. wp_alloc l as "Hl".
+    iIntros (Φ) "_ HΦ". rewrite /newcounter /=. wp_lam. wp_alloc l as "Hl".
     iMod (own_alloc (● (MaxNat O) ⋅ ◯ (MaxNat O))) as (γ) "[Hγ Hγ']";
       first by apply auth_both_valid_discrete.
     iMod (inv_alloc N _ (mcounter_inv γ l) with "[Hl Hγ]").
@@ -114,7 +114,7 @@ Section contrib_spec.
     {{{ True }}} newcounter #()
     {{{ γ l, RET #l; ccounter_ctx γ l ∗ ccounter γ 1 0 }}}.
   Proof.
-    iIntros (Φ) "_ HΦ". rewrite -wp_fupd /newcounter /=. wp_lam. wp_alloc l as "Hl".
+    iIntros (Φ) "_ HΦ". rewrite /newcounter /=. wp_lam. wp_alloc l as "Hl".
     iMod (own_alloc (●F O ⋅ ◯F 0)) as (γ) "[Hγ Hγ']";
       first by apply auth_both_valid_discrete.
     iMod (inv_alloc N _ (ccounter_inv γ l) with "[Hl Hγ]").
diff --git a/iris_heap_lang/lib/spin_lock.v b/iris_heap_lang/lib/spin_lock.v
index 5fcfeed6191e751d652e77f639bbaf05e0048f28..61afd495abc791cb14a8382f2ae9a493003d7e2f 100644
--- a/iris_heap_lang/lib/spin_lock.v
+++ b/iris_heap_lang/lib/spin_lock.v
@@ -59,7 +59,7 @@ Section proof.
   Lemma newlock_spec (R : iProp Σ):
     {{{ R }}} newlock #() {{{ lk γ, RET lk; is_lock γ lk R }}}.
   Proof.
-    iIntros (Φ) "HR HΦ". rewrite -wp_fupd /newlock /=.
+    iIntros (Φ) "HR HΦ". rewrite /newlock /=.
     wp_lam. wp_alloc l as "Hl".
     iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
     iMod (inv_alloc N _ (lock_inv γ l R) with "[-HΦ]") as "#?".
diff --git a/iris_heap_lang/lib/ticket_lock.v b/iris_heap_lang/lib/ticket_lock.v
index 55856b30467f3adc3694787e031d81c5a31e306f..a464b44a5ee5b28e91f5dc80ae31f770045c194f 100644
--- a/iris_heap_lang/lib/ticket_lock.v
+++ b/iris_heap_lang/lib/ticket_lock.v
@@ -82,7 +82,7 @@ Section proof.
   Lemma newlock_spec (R : iProp Σ) :
     {{{ R }}} newlock #() {{{ lk γ, RET lk; is_lock γ lk R }}}.
   Proof.
-    iIntros (Φ) "HR HΦ". rewrite -wp_fupd. wp_lam.
+    iIntros (Φ) "HR HΦ". wp_lam.
     wp_alloc ln as "Hln". wp_alloc lo as "Hlo".
     iMod (own_alloc (● (Excl' 0, GSet ∅) ⋅ ◯ (Excl' 0, GSet ∅))) as (γ) "[Hγ Hγ']".
     { by apply auth_both_valid_discrete. }
diff --git a/tests/ipm_paper.v b/tests/ipm_paper.v
index 5895fe954477bdabba737c7ec8c7afb8b27d13d4..c5b7ed8243ff4a31665115656d71683f5daf6c7e 100644
--- a/tests/ipm_paper.v
+++ b/tests/ipm_paper.v
@@ -204,7 +204,7 @@ Section counter_proof.
   Lemma newcounter_spec :
     ⊢ {{ True }} newcounter #() {{ v, ∃ l, ⌜v = #l⌝ ∧ C l 0 }}.
   Proof.
-    iIntros "!> _ /=". rewrite -wp_fupd /newcounter /=. wp_lam. wp_alloc l as "Hl".
+    iIntros "!> _ /=". rewrite /newcounter /=. wp_lam. wp_alloc l as "Hl".
     iMod (own_alloc (Auth 0)) as (γ) "Hγ"; first done.
     rewrite (auth_frag_op 0 0) //; iDestruct "Hγ" as "[Hγ Hγf]".
     set (N:= nroot .@ "counter").
diff --git a/tests/one_shot.v b/tests/one_shot.v
index cec2f71d4bb4178adaba7b502066e9559c11a9e7..b859132b9820f1aec3421f6f1faf248dd0848be0 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -47,7 +47,7 @@ Lemma wp_one_shot (Φ : val → iProp Σ) :
   ⊢ WP one_shot_example #() {{ Φ }}.
 Proof.
   iIntros "Hf /=". pose proof (nroot .@ "N") as N.
-  rewrite -wp_fupd. wp_lam. wp_alloc l as "Hl".
+  wp_lam. wp_alloc l as "Hl".
   iMod (own_alloc Pending) as (γ) "Hγ"; first done.
   iMod (inv_alloc N _ (one_shot_inv γ l) with "[Hl Hγ]") as "#HN".
   { iNext. iLeft. by iSplitL "Hl". }
diff --git a/tests/one_shot_once.v b/tests/one_shot_once.v
index e2fb69892d6938a7f1c9ed5a391ef30d95459d44..5ce48658c5f1a5b7c4e98ec4b0292de1dd9d24de 100644
--- a/tests/one_shot_once.v
+++ b/tests/one_shot_once.v
@@ -61,7 +61,7 @@ Lemma wp_one_shot (Φ : val → iProp Σ) :
   ⊢ WP one_shot_example #() {{ Φ }}.
 Proof.
   iIntros "Hf /=". pose proof (nroot .@ "N") as N.
-  rewrite -wp_fupd. wp_lam. wp_alloc l as "Hl".
+  wp_lam. wp_alloc l as "Hl".
   iMod (own_alloc (Pending 1%Qp)) as (γ) "Hγ"; first done.
   iDestruct (pending_split with "Hγ") as "[Hγ1 Hγ2]".
   iMod (inv_alloc N _ (one_shot_inv γ l) with "[Hl Hγ2]") as "#HN".