diff --git a/heap_lang/lib/assert.v b/heap_lang/lib/assert.v
index 5b454b0be362b1ef5ef5b0e67145d86999667af3..b222b908ddd29472e2f3aee7fadea1be89368a2e 100644
--- a/heap_lang/lib/assert.v
+++ b/heap_lang/lib/assert.v
@@ -13,5 +13,5 @@ Lemma wp_assert `{heapG Σ} E (Φ : val → iProp Σ) e `{!Closed [] e} :
   WP e @ E {{ v, v = #true ∧ ▷ Φ #() }} ⊢ WP assert: e @ E {{ Φ }}.
 Proof.
   iIntros "HΦ". rewrite /assert. wp_let. wp_seq.
-  iApply (wp_wand_r with "[- $HΦ]"). iIntros (v) "[% ?]"; subst. by wp_if.
+  iApply (wp_wand with "HΦ"). iIntros (v) "[% ?]"; subst. by wp_if.
 Qed.
diff --git a/heap_lang/lib/par.v b/heap_lang/lib/par.v
index ad5f70a67708412d0f2e5d37911ae4df62678ee9..52eae597b108dfdbbde653fc3edfb4966fdf4c12 100644
--- a/heap_lang/lib/par.v
+++ b/heap_lang/lib/par.v
@@ -30,7 +30,7 @@ Proof.
   rewrite /par. wp_value. wp_let. wp_proj.
   wp_apply (spawn_spec parN with "[$Hh $Hf1]"); try wp_done; try solve_ndisj.
   iIntros (l) "Hl". wp_let. wp_proj. wp_bind (f2 _).
-  iApply (wp_wand_r with "[- $Hf2]"); iIntros (v) "H2". wp_let.
+  iApply (wp_wand with "Hf2"); iIntros (v) "H2". wp_let.
   wp_apply (join_spec with "[$Hl]"). iIntros (w) "H1".
   iSpecialize ("HΦ" with "* [-]"); first by iSplitL "H1". by wp_let.
 Qed.
diff --git a/heap_lang/lib/spawn.v b/heap_lang/lib/spawn.v
index 4736671187a35356befafcf0553243ffd5bba9b6..8e2e167888eff87cd512bddc4f039b7e03a0c9ce 100644
--- a/heap_lang/lib/spawn.v
+++ b/heap_lang/lib/spawn.v
@@ -58,7 +58,7 @@ Proof.
   { iNext. iExists NONEV. iFrame; eauto. }
   wp_apply wp_fork; simpl. iSplitR "Hf".
   - wp_seq. iApply "HΦ". rewrite /join_handle. eauto.
-  - wp_bind (f _). iApply (wp_wand_r with "[ $Hf]"); iIntros (v) "Hv".
+  - wp_bind (f _). iApply (wp_wand with "Hf"); iIntros (v) "Hv".
     iInv N as (v') "[Hl _]" "Hclose".
     wp_store. iApply "Hclose". iNext. iExists (SOMEV v). iFrame. eauto.
 Qed.
diff --git a/program_logic/hoare.v b/program_logic/hoare.v
index 8fcb0ec3cae82267ab3b4132e493e943f039e038..0f8b104df742cb9e160d8ec4bde0466ccb60865b 100644
--- a/program_logic/hoare.v
+++ b/program_logic/hoare.v
@@ -64,7 +64,7 @@ Lemma ht_vs E P P' Φ Φ' e :
   ⊢ {{ P }} e @ E {{ Φ }}.
 Proof.
   iIntros "(#Hvs & #Hwp & #HΦ) !# HP". iMod ("Hvs" with "HP") as "HP".
-  iApply wp_fupd; iApply wp_wand_r; iSplitL; [by iApply "Hwp"|].
+  iApply wp_fupd. iApply (wp_wand with "[HP]"); [by iApply "Hwp"|].
   iIntros (v) "Hv". by iApply "HΦ".
 Qed.
 
@@ -75,7 +75,7 @@ Lemma ht_atomic E1 E2 P P' Φ Φ' e :
 Proof.
   iIntros (?) "(#Hvs & #Hwp & #HΦ) !# HP". iApply (wp_atomic _ E2); auto.
   iMod ("Hvs" with "HP") as "HP". iModIntro.
-  iApply wp_wand_r; iSplitL; [by iApply "Hwp"|].
+  iApply (wp_wand with "[HP]"); [by iApply "Hwp"|].
   iIntros (v) "Hv". by iApply "HΦ".
 Qed.
 
@@ -84,7 +84,7 @@ Lemma ht_bind `{LanguageCtx Λ K} E P Φ Φ' e :
   ⊢ {{ P }} K e @ E {{ Φ' }}.
 Proof.
   iIntros "[#Hwpe #HwpK] !# HP". iApply wp_bind.
-  iApply wp_wand_r; iSplitL; [by iApply "Hwpe"|].
+  iApply (wp_wand with "[HP]"); [by iApply "Hwpe"|].
   iIntros (v) "Hv". by iApply "HwpK".
 Qed.
 
diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index 59efd2377b8d71255686ed2a016e43d5c87f4bc5..97fee1f57d03c63c27d5cc392455c1b2a0f3f120 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -275,15 +275,18 @@ Lemma wp_frame_step_r' E e Φ R :
   to_val e = None → WP e @ E {{ Φ }} ∗ ▷ R ⊢ WP e @ E {{ v, Φ v ∗ R }}.
 Proof. iIntros (?) "[??]". iApply (wp_frame_step_r E E); try iFrame; eauto. Qed.
 
-Lemma wp_wand_l E e Φ Ψ :
-  (∀ v, Φ v -∗ Ψ v) ∗ WP e @ E {{ Φ }} ⊢ WP e @ E {{ Ψ }}.
+Lemma wp_wand E e Φ Ψ :
+  WP e @ E {{ Φ }} ⊢ (∀ v, Φ v -∗ Ψ v) -∗ WP e @ E {{ Ψ }}.
 Proof.
-  iIntros "[H Hwp]". iApply (wp_strong_mono E); auto.
+  iIntros "Hwp H". iApply (wp_strong_mono E); auto.
   iFrame "Hwp". iIntros (?) "?". by iApply "H".
 Qed.
+Lemma wp_wand_l E e Φ Ψ :
+  (∀ v, Φ v -∗ Ψ v) ∗ WP e @ E {{ Φ }} ⊢ WP e @ E {{ Ψ }}.
+Proof. iIntros "[H Hwp]". iApply (wp_wand with "Hwp H"). Qed.
 Lemma wp_wand_r E e Φ Ψ :
   WP e @ E {{ Φ }} ∗ (∀ v, Φ v -∗ Ψ v) ⊢ WP e @ E {{ Ψ }}.
-Proof. by rewrite comm wp_wand_l. Qed.
+Proof. iIntros "[Hwp H]". iApply (wp_wand with "Hwp H"). Qed.
 End wp.
 
 (** Proofmode class instances *)
diff --git a/tests/barrier_client.v b/tests/barrier_client.v
index 408bb502c4c4878483e50496da70096f99b03de4..a4b7e564d5d291461cd37d232a4fd8d3894cdb0e 100644
--- a/tests/barrier_client.v
+++ b/tests/barrier_client.v
@@ -31,7 +31,7 @@ Section client.
     iIntros "[#Hh Hrecv]". wp_lam. wp_let.
     wp_apply (wait_spec with "[- $Hrecv]"). iDestruct 1 as (f) "[Hy #Hf]".
     wp_seq. wp_load.
-    iApply wp_wand_r. iSplitR; [iApply "Hf"|by iIntros (v) "_"].
+    iApply (wp_wand with "[]"). iApply "Hf". by iIntros (v) "_".
   Qed.
 
   Lemma client_safe : heapN ⊥ N → heap_ctx ⊢ WP client {{ _, True }}.
diff --git a/tests/joining_existentials.v b/tests/joining_existentials.v
index 0652b491f67f53094b88b88e5c73764ec95f11c3..0c3f3cb3f6d473b436e751e23c803cc2c6f9f378 100644
--- a/tests/joining_existentials.v
+++ b/tests/joining_existentials.v
@@ -37,7 +37,7 @@ Lemma worker_spec e γ l (Φ Ψ : X → iProp Σ) `{!Closed [] e} :
 Proof.
   iIntros "[Hl #He]". wp_apply (wait_spec with "[- $Hl]"); simpl.
   iDestruct 1 as (x) "[#Hγ Hx]".
-  wp_seq. iApply wp_wand_l. iSplitR; [|by iApply "He"].
+  wp_seq. iApply (wp_wand with "[Hx]"); [by iApply "He"|].
   iIntros (v) "?"; iExists x; by iSplit.
 Qed.
 
@@ -81,7 +81,7 @@ Proof.
   set (workers_post (v : val) := (barrier_res γ Ψ1 ∗ barrier_res γ Ψ2)%I).
   wp_let. wp_apply (wp_par  (λ _, True)%I workers_post with "[- $Hh]").
   iSplitL "HP Hs Hγ"; [|iSplitL "Hr"].
-  - wp_bind eM. iApply wp_wand_l; iSplitR "HP"; [|by iApply "He"].
+  - wp_bind eM. iApply (wp_wand with "[HP]"); [by iApply "He"|].
     iIntros (v) "HP"; iDestruct "HP" as (x) "HP". wp_let.
     iMod (own_update with "Hγ") as "Hx".
     { by apply (cmra_update_exclusive (Shot x)). }
diff --git a/tests/one_shot.v b/tests/one_shot.v
index dea6c813d7ce326c0087245b6843283e091afca9..aa97d00877c7167919a90d0de650db3000fdd044 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -94,6 +94,6 @@ Proof.
   iIntros (f1 f2) "[#Hf1 #Hf2]"; iSplit.
   - iIntros (n) "!# _". wp_proj. iApply "Hf1".
   - iIntros "!# _". wp_proj.
-    iApply (wp_wand_r with "[- $Hf2]"). by iIntros (v) "#? !# _".
+    iApply (wp_wand with "Hf2"). by iIntros (v) "#? !# _".
 Qed.
 End proof.