diff --git a/CHANGELOG.md b/CHANGELOG.md
index f07e719dce927af0b0296b4010a70a165c05b854..44b2615815e09b6f48146807e01247c05f5d96dd 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -56,6 +56,7 @@ Coq 8.11 is no longer supported in this version of Iris.
    - Use `fupd_intro _ _` for the new field `state_interp_mono` of `irisG`.
    - Some proofs using lifting lemmas and adequacy theorems need to be adapted
      to ignore the new step counter.
+* Remove `wp_frame_wand_l`; add `wp_frame_wand` as more symmetric replacement.
 
 **Changes in `heap_lang`:**
 
diff --git a/iris/program_logic/atomic.v b/iris/program_logic/atomic.v
index 04a07d03ef49c36280da23a82ed4f7c72a028d7a..63f075cbc2436feacc7b07b1e711bbebbd6bd008 100644
--- a/iris/program_logic/atomic.v
+++ b/iris/program_logic/atomic.v
@@ -112,7 +112,7 @@ Section lemmas.
     ∀ Φ, ∀.. x, α x -∗ (∀.. y, β x y -∗ Φ (f x y)) -∗ WP e {{ Φ }}.
   Proof.
     rewrite ->tforall_forall in HL. iIntros "Hwp" (Φ x) "Hα HΦ".
-    iApply wp_frame_wand_l. iSplitL "HΦ"; first iAccu. iApply "Hwp".
+    iApply (wp_frame_wand with "HΦ"). iApply "Hwp".
     iAuIntro. iAaccIntro with "Hα"; first by eauto. iIntros (y) "Hβ !>".
     (* FIXME: Using ssreflect rewrite does not work, see Coq bug #7773. *)
     rewrite ->!tele_app_bind. iIntros "HΦ". iApply "HΦ". done.
diff --git a/iris/program_logic/total_weakestpre.v b/iris/program_logic/total_weakestpre.v
index 6278dc971dbcbdf978cf2e3ac32a194514af81c8..f2fd5b3e1c16549a92d1431335726e7283d1c18a 100644
--- a/iris/program_logic/total_weakestpre.v
+++ b/iris/program_logic/total_weakestpre.v
@@ -257,6 +257,12 @@ Proof. iIntros "[H Hwp]". iApply (twp_wand with "Hwp H"). Qed.
 Lemma twp_wand_r s E e Φ Ψ :
   WP e @ s; E [{ Φ }] ∗ (∀ v, Φ v -∗ Ψ v) -∗ WP e @ s; E [{ Ψ }].
 Proof. iIntros "[Hwp H]". iApply (twp_wand with "Hwp H"). Qed.
+Lemma twp_frame_wand s E e Φ R :
+  R -∗ WP e @ s; E [{ v, R -∗ Φ v }] -∗ WP e @ s; E [{ Φ }].
+Proof.
+  iIntros "HR HWP". iApply (twp_wand with "HWP").
+  iIntros (v) "HΦ". by iApply "HΦ".
+Qed.
 
 Lemma twp_wp_step s E e P Φ :
   TCEq (to_val e) None →
diff --git a/iris/program_logic/weakestpre.v b/iris/program_logic/weakestpre.v
index 3f97d83d401890011fe063f0bb0f7f336e3f209d..883d401af9e682b85437a556ca9c76d7b43c3e4f 100644
--- a/iris/program_logic/weakestpre.v
+++ b/iris/program_logic/weakestpre.v
@@ -348,10 +348,10 @@ Proof. iIntros "[H Hwp]". iApply (wp_wand with "Hwp H"). Qed.
 Lemma wp_wand_r s E e Φ Ψ :
   WP e @ s; E {{ Φ }} ∗ (∀ v, Φ v -∗ Ψ v) ⊢ WP e @ s; E {{ Ψ }}.
 Proof. iIntros "[Hwp H]". iApply (wp_wand with "Hwp H"). Qed.
-Lemma wp_frame_wand_l s E e Q Φ :
-  Q ∗ WP e @ s; E {{ v, Q -∗ Φ v }} -∗ WP e @ s; E {{ Φ }}.
+Lemma wp_frame_wand s E e Φ R :
+  R -∗ WP e @ s; E {{ v, R -∗ Φ v }} -∗ WP e @ s; E {{ Φ }}.
 Proof.
-  iIntros "[HQ HWP]". iApply (wp_wand with "HWP").
+  iIntros "HR HWP". iApply (wp_wand with "HWP").
   iIntros (v) "HΦ". by iApply "HΦ".
 Qed.
 End wp.
diff --git a/iris_heap_lang/proofmode.v b/iris_heap_lang/proofmode.v
index ab4d717041fb158023d6ea3fae514d4a752457a1..55314fede036babd02bb1bd11703d7b12d55089a 100644
--- a/iris_heap_lang/proofmode.v
+++ b/iris_heap_lang/proofmode.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import coq_tactics reduction.
+From iris.proofmode Require Import coq_tactics reduction spec_patterns.
 From iris.proofmode Require Export tactics.
 From iris.program_logic Require Import atomic.
 From iris.heap_lang Require Export tactics derived_laws.
@@ -556,9 +556,13 @@ Tactic Notation "awp_apply" open_constr(lem) :=
   wp_apply_core lem ltac:(fun H => iApplyHyp H) ltac:(fun cont => fail);
   last iAuIntro.
 Tactic Notation "awp_apply" open_constr(lem) "without" constr(Hs) :=
+  (* Convert "list of hypothesis" into specialization pattern. *)
+  let Hs := words Hs in
+  let Hs := eval vm_compute in (INamed <$> Hs) in
   wp_apply_core lem
     ltac:(fun H =>
-      iApply wp_frame_wand_l; iSplitL Hs; [iAccu|iApplyHyp H]) 
+      iApply (wp_frame_wand with
+        [SGoal $ SpecGoal GSpatial false [] Hs false]); [iAccu|iApplyHyp H])
     ltac:(fun cont => fail);
   last iAuIntro.