diff --git a/program_logic/pviewshifts.v b/program_logic/pviewshifts.v
index 055b485a91cb39eb293d8ccb2421197c05317f01..586777c6fe9cbab329b0d3c0b461027510738365 100644
--- a/program_logic/pviewshifts.v
+++ b/program_logic/pviewshifts.v
@@ -31,6 +31,10 @@ Notation "P ={ E }=★ Q" := (P -★ |={E}=> Q)%I
 Notation "P ={ E }=> Q" := (P ⊢ |={E}=> Q)
   (at level 99, E at level 50, Q at level 200, only parsing) : C_scope.
 
+Notation "|={ E1 , E2 }â–·=> Q" := (|={E1%I,E2%I}=> â–· |={E2,E1}=> Q)%I
+  (at level 99, E1, E2 at level 50, Q at level 200,
+   format "|={ E1 , E2 }â–·=>  Q") : uPred_scope.
+
 Section pvs.
 Context `{irisG Λ Σ}.
 Implicit Types P Q : iProp Σ.
diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index b805f323962d873e45ae20f90e88dd1d509fb4a5..38665fe9fd910cde604a8573f746c1e76927c641 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -134,7 +134,7 @@ Qed.
 
 Lemma wp_frame_step_l E1 E2 e Φ R :
   to_val e = None → E2 ⊆ E1 →
-  (|={E1,E2}=> ▷ |={E2,E1}=> R) ★ WP e @ E2 {{ Φ }} ⊢ WP e @ E1 {{ v, R ★ Φ v }}.
+  (|={E1,E2}▷=> R) ★ WP e @ E2 {{ Φ }} ⊢ WP e @ E1 {{ v, R ★ Φ v }}.
 Proof.
   rewrite !wp_unfold /wp_pre. iIntros (??) "[HR [Hv|[_ H]]]".
   { iDestruct "Hv" as (v) "[% Hv]"; simplify_eq. }
@@ -189,7 +189,7 @@ Proof. iIntros "[??]". iApply (wp_strong_mono E E _ Φ); try iFrame; eauto. Qed.
 
 Lemma wp_frame_step_r E1 E2 e Φ R :
   to_val e = None → E2 ⊆ E1 →
-  WP e @ E2 {{ Φ }} ★ (|={E1,E2}=> ▷ |={E2,E1}=> R) ⊢ WP e @ E1 {{ v, Φ v ★ R }}.
+  WP e @ E2 {{ Φ }} ★ (|={E1,E2}▷=> R) ⊢ WP e @ E1 {{ v, Φ v ★ R }}.
 Proof.
   rewrite [(WP _ @ _ {{ _ }} ★ _)%I]comm; setoid_rewrite (comm _ _ R).
   apply wp_frame_step_l.