diff --git a/algebra/upred.v b/algebra/upred.v
index 8f53aca1ead452fedac0021ca08195ebc3e2cb49..e0a9e313f742e61905f5463b5115a1cb5a02c0d8 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -276,6 +276,7 @@ Notation "(⊣⊢)" := (equiv (A:=uPred _)) (only parsing) : C_scope.
 Notation "■ φ" := (uPred_const φ%C%type)
   (at level 20, right associativity) : uPred_scope.
 Notation "x = y" := (uPred_const (x%C%type = y%C%type)) : uPred_scope.
+Notation "x ⊥ y" := (uPred_const (x%C%type ⊥ y%C%type)) : uPred_scope.
 Notation "'False'" := (uPred_const False) : uPred_scope.
 Notation "'True'" := (uPred_const True) : uPred_scope.
 Infix "∧" := uPred_and : uPred_scope.
diff --git a/heap_lang/lib/assert.v b/heap_lang/lib/assert.v
index 705282b5d4040c3d87ff4ad061c5f9633909db37..1f12a4ef0f5940d05aa8fb13d518e8f04127a776 100644
--- a/heap_lang/lib/assert.v
+++ b/heap_lang/lib/assert.v
@@ -16,7 +16,7 @@ Lemma wp_assert {Σ} (Φ : val → iProp heap_lang Σ) :
 Proof. by rewrite -wp_if_true -wp_value. Qed.
 
 Lemma wp_assert' {Σ} (Φ : val → iProp heap_lang Σ) e :
-  WP e {{ λ v, v = #true ∧ ▷ Φ #() }} ⊢ WP Assert e {{ Φ }}.
+  WP e {{ v, v = #true ∧ ▷ Φ #() }} ⊢ WP Assert e {{ Φ }}.
 Proof.
   rewrite /Assert. wp_focus e; apply wp_mono=>v.
   apply uPred.const_elim_l=>->. apply wp_assert.
diff --git a/heap_lang/lib/barrier/client.v b/heap_lang/lib/barrier/client.v
index d8d302b35cbac9690c8105dd4f7e63fbdd8080d7..a0e32df072e9bb349352f4d8ae59299f04f3fc8c 100644
--- a/heap_lang/lib/barrier/client.v
+++ b/heap_lang/lib/barrier/client.v
@@ -17,7 +17,7 @@ Section client.
   Local Notation iProp := (iPropG heap_lang Σ).
 
   Definition y_inv (q : Qp) (l : loc) : iProp :=
-    (∃ f : val, l ↦{q} f ★ □ ∀ n : Z, WP f #n {{ λ v, v = #(n + 42) }})%I.
+    (∃ f : val, l ↦{q} f ★ □ ∀ n : Z, WP f #n {{ v, v = #(n + 42) }})%I.
 
   Lemma y_inv_split q l : y_inv q l ⊢ (y_inv (q/2) l ★ y_inv (q/2) l).
   Proof.
@@ -27,7 +27,7 @@ Section client.
 
   Lemma worker_safe q (n : Z) (b y : loc) :
     (heap_ctx heapN ★ recv heapN N b (y_inv q y))
-    ⊢ WP worker n (%b) (%y) {{ λ _, True }}.
+    ⊢ WP worker n (%b) (%y) {{ _, True }}.
   Proof.
     iIntros "[#Hh Hrecv]". wp_lam. wp_let.
     wp_apply wait_spec; iFrame "Hrecv".
@@ -36,7 +36,7 @@ Section client.
     iApply wp_wand_r; iSplitR; [iApply "Hf"|by iIntros {v} "_"].
   Qed.
 
-  Lemma client_safe : heapN ⊥ N → heap_ctx heapN ⊢ WP client {{ λ _, True }}.
+  Lemma client_safe : heapN ⊥ N → heap_ctx heapN ⊢ WP client {{ _, True }}.
   Proof.
     iIntros {?} "#Hh"; rewrite /client. wp_alloc y as "Hy". wp_let.
     wp_apply (newbarrier_spec heapN N (y_inv 1 y)); first done.
@@ -61,7 +61,7 @@ Section ClosedProofs.
   Definition Σ : gFunctors := #[ heapGF ; barrierGF ; spawnGF ].
   Notation iProp := (iPropG heap_lang Σ).
 
-  Lemma client_safe_closed σ : {{ ownP σ : iProp }} client {{ λ v, True }}.
+  Lemma client_safe_closed σ : {{ ownP σ : iProp }} client {{ v, True }}.
   Proof.
     iIntros "! Hσ".
     iPvs (heap_alloc (nroot .@ "Barrier")) "Hσ" as {h} "[#Hh _]"; first done.
diff --git a/heap_lang/lib/barrier/specification.v b/heap_lang/lib/barrier/specification.v
index cdb18b49523507a842b4ea1534628afb853fd9a3..f3973ad1b11f35121647b6a15c5275fe977c6ef5 100644
--- a/heap_lang/lib/barrier/specification.v
+++ b/heap_lang/lib/barrier/specification.v
@@ -13,10 +13,10 @@ Local Notation iProp := (iPropG heap_lang Σ).
 Lemma barrier_spec (heapN N : namespace) :
   heapN ⊥ N →
   ∃ recv send : loc → iProp -n> iProp,
-    (∀ P, heap_ctx heapN ⊢ {{ True }} newbarrier #() {{ λ v,
+    (∀ P, heap_ctx heapN ⊢ {{ True }} newbarrier #() {{ v,
                              ∃ l : loc, v = LocV l ★ recv l P ★ send l P }}) ∧
-    (∀ l P, {{ send l P ★ P }} signal (LocV l) {{ λ _, True }}) ∧
-    (∀ l P, {{ recv l P }} wait (LocV l) {{ λ _, P }}) ∧
+    (∀ l P, {{ send l P ★ P }} signal (LocV l) {{ _, True }}) ∧
+    (∀ l P, {{ recv l P }} wait (LocV l) {{ _, P }}) ∧
     (∀ l P Q, recv l (P ★ Q) ={N}=> recv l P ★ recv l Q) ∧
     (∀ l P Q, (P -★ Q) ⊢ (recv l P -★ recv l Q)).
 Proof.
diff --git a/heap_lang/lib/lock.v b/heap_lang/lib/lock.v
index a74e0ad5f55bf5278e3b6056a811087be2fcff8c..9de604041ae5340936cbf77d52798e9918db850d 100644
--- a/heap_lang/lib/lock.v
+++ b/heap_lang/lib/lock.v
@@ -24,10 +24,10 @@ Definition lock_inv (γ : gname) (l : loc) (R : iProp) : iProp :=
   (∃ b : bool, l ↦ #b ★ if b then True else own γ (Excl ()) ★ R)%I.
 
 Definition is_lock (l : loc) (R : iProp) : iProp :=
-  (∃ N γ, ■ (heapN ⊥ N) ∧ heap_ctx heapN ∧ inv N (lock_inv γ l R))%I.
+  (∃ N γ, heapN ⊥ N ∧ heap_ctx heapN ∧ inv N (lock_inv γ l R))%I.
 
 Definition locked (l : loc) (R : iProp) : iProp :=
-  (∃ N γ, ■ (heapN ⊥ N) ∧ heap_ctx heapN ∧
+  (∃ N γ, heapN ⊥ N ∧ heap_ctx heapN ∧
           inv N (lock_inv γ l R) ∧ own γ (Excl ()))%I.
 
 Global Instance lock_inv_ne n γ l : Proper (dist n ==> dist n) (lock_inv γ l).
diff --git a/heap_lang/lib/spawn.v b/heap_lang/lib/spawn.v
index 52208d3af21aa488e74f32fc9b8782a225fd7156..5172ea364f5e4599804d51b34e5ef8e3e7483c13 100644
--- a/heap_lang/lib/spawn.v
+++ b/heap_lang/lib/spawn.v
@@ -37,8 +37,8 @@ Definition spawn_inv (γ : gname) (l : loc) (Ψ : val → iProp) : iProp :=
                    ∃ v, lv = InjRV v ★ (Ψ v ∨ own γ (Excl ()))))%I.
 
 Definition join_handle (l : loc) (Ψ : val → iProp) : iProp :=
-  (■ (heapN ⊥ N) ★ ∃ γ, heap_ctx heapN ★ own γ (Excl ()) ★
-                        inv N (spawn_inv γ l Ψ))%I.
+  (heapN ⊥ N ★ ∃ γ, heap_ctx heapN ★ own γ (Excl ()) ★
+                    inv N (spawn_inv γ l Ψ))%I.
 
 Typeclasses Opaque join_handle.
 
diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v
index 9acaae28dc8e391dfbdf149172963b81a814675c..3735ab340a9c8b67c167fcfa2c40b7c61ff47a68 100644
--- a/heap_lang/lifting.v
+++ b/heap_lang/lifting.v
@@ -13,11 +13,11 @@ Implicit Types ef : option (expr []).
 
 (** Bind. This bundles some arguments that wp_ectx_bind leaves as indices. *)
 Lemma wp_bind {E e} K Φ :
-  WP e @ E {{ λ v, WP fill K (of_val v) @ E {{ Φ }} }} ⊢ WP fill K e @ E {{ Φ }}.
+  WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }} ⊢ WP fill K e @ E {{ Φ }}.
 Proof. exact: wp_ectx_bind. Qed.
 
 Lemma wp_bindi {E e} Ki Φ :
-  WP e @ E {{ λ v, WP fill_item Ki (of_val v) @ E {{ Φ }} }} ⊢
+  WP e @ E {{ v, WP fill_item Ki (of_val v) @ E {{ Φ }} }} ⊢
      WP fill_item Ki e @ E {{ Φ }}.
 Proof. exact: weakestpre.wp_bind. Qed.
 
@@ -81,7 +81,7 @@ Qed.
 
 (** Base axioms for core primitives of the language: Stateless reductions *)
 Lemma wp_fork E e Φ :
-  (▷ Φ (LitV LitUnit) ★ ▷ WP e {{ λ _, True }}) ⊢ WP Fork e @ E {{ Φ }}.
+  (▷ Φ (LitV LitUnit) ★ ▷ WP e {{ _, True }}) ⊢ WP Fork e @ E {{ Φ }}.
 Proof.
   rewrite -(wp_lift_pure_det_head_step (Fork e) (Lit LitUnit) (Some e)) //=;
     last by intros; inv_head_step; eauto.
diff --git a/heap_lang/notation.v b/heap_lang/notation.v
index b69fb3602f720c8d559850ce31fc037dfebca481..bbe0624c8c01790f2236e32b6ad93f7b007c6687 100644
--- a/heap_lang/notation.v
+++ b/heap_lang/notation.v
@@ -2,6 +2,7 @@ From iris.heap_lang Require Export derived.
 Export heap_lang.
 
 Arguments wp {_ _} _ _%E _.
+
 Notation "'WP' e @ E {{ Φ } }" := (wp E e%E Φ)
   (at level 20, e, Φ at level 200,
    format "'WP'  e  @  E  {{  Φ  } }") : uPred_scope.
@@ -9,6 +10,13 @@ Notation "'WP' e {{ Φ } }" := (wp ⊤ e%E Φ)
   (at level 20, e, Φ at level 200,
    format "'WP'  e  {{  Φ  } }") : uPred_scope.
 
+Notation "'WP' e @ E {{ v , Q } }" := (wp E e%E (λ v, Q))
+  (at level 20, e, Q at level 200,
+   format "'WP'  e  @  E  {{  v ,  Q  } }") : uPred_scope.
+Notation "'WP' e {{ v , Q } }" := (wp ⊤ e%E (λ v, Q))
+  (at level 20, e, Q at level 200,
+   format "'WP'  e  {{  v ,  Q  } }") : uPred_scope.
+
 Coercion LitInt : Z >-> base_lit.
 Coercion LitBool : bool >-> base_lit.
 Coercion App : expr >-> Funclass.
diff --git a/program_logic/adequacy.v b/program_logic/adequacy.v
index fa9003c047e434f9cfbc2ad94308a2f7cc7e52b4..9e364ca60c8d843acfb78b7f574c4258ef97fb0c 100644
--- a/program_logic/adequacy.v
+++ b/program_logic/adequacy.v
@@ -84,7 +84,7 @@ Qed.
 
 Theorem wp_adequacy_result E φ e v t2 σ1 m σ2 :
   ✓ m →
-  (ownP σ1 ★ ownG m) ⊢ WP e @ E {{ λ v', ■ φ v' }} →
+  (ownP σ1 ★ ownG m) ⊢ WP e @ E {{ v', ■ φ v' }} →
   rtc step ([e], σ1) (of_val v :: t2, σ2) →
   φ v.
 Proof.
@@ -100,7 +100,7 @@ Qed.
 
 Lemma ht_adequacy_result E φ e v t2 σ1 m σ2 :
   ✓ m →
-  {{ ownP σ1 ★ ownG m }} e @ E {{ λ v', ■ φ v' }} →
+  {{ ownP σ1 ★ ownG m }} e @ E {{ v', ■ φ v' }} →
   rtc step ([e], σ1) (of_val v :: t2, σ2) →
   φ v.
 Proof.
diff --git a/program_logic/ectx_weakestpre.v b/program_logic/ectx_weakestpre.v
index 146ab2e179558ba1cb86be00a2fd912fbb5cd451..07a5f07f6ec4c180b72723946e05c12bd661b36d 100644
--- a/program_logic/ectx_weakestpre.v
+++ b/program_logic/ectx_weakestpre.v
@@ -14,7 +14,7 @@ Hint Resolve head_prim_reducible head_reducible_prim_step.
 Notation wp_fork ef := (default True ef (flip (wp ⊤) (λ _, True)))%I.
 
 Lemma wp_ectx_bind {E e} K Φ :
-  WP e @ E {{ λ v, WP fill K (of_val v) @ E {{ Φ }} }} ⊢ WP fill K e @ E {{ Φ }}.
+  WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }} ⊢ WP fill K e @ E {{ Φ }}.
 Proof. apply: weakestpre.wp_bind. Qed.
 
 Lemma wp_lift_head_step E1 E2
diff --git a/program_logic/hoare.v b/program_logic/hoare.v
index dcbd755b6e7e2ed1cfd966592652cf927af2978f..84346a0a095f8e860fe3c57343105cc5c1fb06a5 100644
--- a/program_logic/hoare.v
+++ b/program_logic/hoare.v
@@ -19,6 +19,19 @@ Notation "{{ P } } e {{ Φ } }" := (True ⊢ ht ⊤ P e Φ)
   (at level 20, P, e, Φ at level 200,
    format "{{  P  } }  e  {{  Φ  } }") : C_scope.
 
+Notation "{{ P } } e @ E {{ v , Q } }" := (ht E P e (λ v, Q))
+  (at level 20, P, e, Q at level 200,
+   format "{{  P  } }  e  @  E  {{  v ,  Q  } }") : uPred_scope.
+Notation "{{ P } } e {{ v , Q } }" := (ht ⊤ P e (λ v, Q))
+  (at level 20, P, e, Q at level 200,
+   format "{{  P  } }  e  {{  v ,  Q  } }") : uPred_scope.
+Notation "{{ P } } e @ E {{ v , Q } }" := (True ⊢ ht E P e (λ v, Q))
+  (at level 20, P, e, Q at level 200,
+   format "{{  P  } }  e  @  E  {{  v ,  Q  } }") : C_scope.
+Notation "{{ P } } e {{ v , Q } }" := (True ⊢ ht ⊤ P e (λ v, Q))
+  (at level 20, P, e, Q at level 200,
+   format "{{  P  } }  e  {{  v ,  Q  } }") : C_scope.
+
 Section hoare.
 Context {Λ : language} {Σ : iFunctor}.
 Implicit Types P Q : iProp Λ Σ.
@@ -42,8 +55,7 @@ Proof. solve_proper. Qed.
 Lemma ht_alt E P Φ e : (P ⊢ WP e @ E {{ Φ }}) → {{ P }} e @ E {{ Φ }}.
 Proof. iIntros {Hwp} "! HP". by iApply Hwp. Qed.
 
-Lemma ht_val E v :
-  {{ True : iProp Λ Σ }} of_val v @ E {{ λ v', v = v' }}.
+Lemma ht_val E v : {{ True : iProp Λ Σ }} of_val v @ E {{ v', v = v' }}.
 Proof. iIntros "! _". by iApply wp_value'. Qed.
 
 Lemma ht_vs E P P' Φ Φ' e :
@@ -83,13 +95,13 @@ Proof.
 Qed.
 
 Lemma ht_frame_l E P Φ R e :
-  {{ P }} e @ E {{ Φ }} ⊢ {{ R ★ P }} e @ E {{ λ v, R ★ Φ v }}.
+  {{ P }} e @ E {{ Φ }} ⊢ {{ R ★ P }} e @ E {{ v, R ★ Φ v }}.
 Proof.
   iIntros "#Hwp ! [HR HP]". iApply wp_frame_l; iFrame "HR". by iApply "Hwp".
 Qed.
 
 Lemma ht_frame_r E P Φ R e :
-  {{ P }} e @ E {{ Φ }} ⊢ {{ P ★ R }} e @ E {{ λ v, Φ v ★ R }}.
+  {{ P }} e @ E {{ Φ }} ⊢ {{ P ★ R }} e @ E {{ v, Φ v ★ R }}.
 Proof. setoid_rewrite (comm _ _ R); apply ht_frame_l. Qed.
 
 Lemma ht_frame_step_l E E1 E2 P R1 R2 R3 e Φ :
@@ -122,7 +134,7 @@ Qed.
 
 Lemma ht_frame_step_l' E P R e Φ :
   to_val e = None →
-  {{ P }} e @ E {{ Φ }} ⊢ {{ ▷ R ★ P }} e @ E {{ λ v, R ★ Φ v }}.
+  {{ P }} e @ E {{ Φ }} ⊢ {{ ▷ R ★ P }} e @ E {{ v, R ★ Φ v }}.
 Proof.
   iIntros {?} "#Hwp ! [HR HP]".
   iApply wp_frame_step_l'; try done. iFrame "HR". by iApply "Hwp".
@@ -130,7 +142,7 @@ Qed.
 
 Lemma ht_frame_step_r' E P Φ R e :
   to_val e = None →
-  {{ P }} e @ E {{ Φ }} ⊢ {{ P ★ ▷ R }} e @ E {{ λ v, Φ v ★ R }}.
+  {{ P }} e @ E {{ Φ }} ⊢ {{ P ★ ▷ R }} e @ E {{ v, Φ v ★ R }}.
 Proof.
   iIntros {?} "#Hwp ! [HP HR]".
   iApply wp_frame_step_r'; try done. iFrame "HR". by iApply "Hwp".
@@ -138,7 +150,7 @@ Qed.
 
 Lemma ht_inv N E P Φ R e :
   atomic e → nclose N ⊆ E →
-  (inv N R ★ {{ ▷ R ★ P }} e @ E ∖ nclose N {{ λ v, ▷ R ★ Φ v }})
+  (inv N R ★ {{ ▷ R ★ P }} e @ E ∖ nclose N {{ v, ▷ R ★ Φ v }})
     ⊢ {{ P }} e @ E {{ Φ }}.
 Proof.
   iIntros {??} "[#? #Hwp] ! HP". eapply wp_inv; eauto.
diff --git a/program_logic/hoare_lifting.v b/program_logic/hoare_lifting.v
index c9db56c66e71e31e573a2dced978a963845a0a34..99ceeee64e6e168fa673d5a7e9bb52c7dc1d4b97 100644
--- a/program_logic/hoare_lifting.v
+++ b/program_logic/hoare_lifting.v
@@ -3,14 +3,14 @@ From iris.program_logic Require Export hoare lifting.
 From iris.program_logic Require Import ownership.
 From iris.proofmode Require Import tactics pviewshifts.
 
-Local Notation "{{ P } } ef ?@ E {{ Φ } }" :=
-  (default True%I ef (λ e, ht E P e Φ))
-  (at level 20, P, ef, Φ at level 200,
-   format "{{  P  } }  ef  ?@  E  {{  Φ  } }") : uPred_scope.
-Local Notation "{{ P } } ef ?@ E {{ Φ } }" :=
-  (True ⊢ default True ef (λ e, ht E P e Φ))
-  (at level 20, P, ef, Φ at level 200,
-   format "{{  P  } }  ef  ?@  E  {{  Φ  } }") : C_scope.
+Local Notation "{{ P } } ef ?@ E {{ v , Q } }" :=
+  (default True%I ef (λ e, ht E P e (λ v, Q)))
+  (at level 20, P, ef, Q at level 200,
+   format "{{  P  } }  ef  ?@  E  {{  v ,  Q  } }") : uPred_scope.
+Local Notation "{{ P } } ef ?@ E {{ v , Q } }" :=
+  (True ⊢ default True ef (λ e, ht E P e (λ v, Q)))
+  (at level 20, P, ef, Q at level 200,
+   format "{{  P  } }  ef  ?@  E  {{  v ,  Q  } }") : C_scope.
 
 Section lifting.
 Context {Λ : language} {Σ : iFunctor}.
@@ -26,7 +26,7 @@ Lemma ht_lift_step E1 E2
   ((P ={E1,E2}=> ▷ ownP σ1 ★ ▷ P') ∧
    (∀ e2 σ2 ef, ■ φ e2 σ2 ef ★ ownP σ2 ★ P' ={E2,E1}=> Φ1 e2 σ2 ef ★ Φ2 e2 σ2 ef) ∧
    (∀ e2 σ2 ef, {{ Φ1 e2 σ2 ef }} e2 @ E1 {{ Ψ }}) ∧
-   (∀ e2 σ2 ef, {{ Φ2 e2 σ2 ef }} ef ?@ ⊤ {{ λ _, True }}))
+   (∀ e2 σ2 ef, {{ Φ2 e2 σ2 ef }} ef ?@ ⊤ {{ _, True }}))
   ⊢ {{ P }} e1 @ E1 {{ Ψ }}.
 Proof.
   iIntros {?? Hsafe Hstep} "#(#Hvs&HΦ&He2&Hef) ! HP".
@@ -45,8 +45,8 @@ Lemma ht_lift_atomic_step
   atomic e1 →
   reducible e1 σ1 →
   (∀ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → φ e2 σ2 ef) →
-  (∀ e2 σ2 ef, {{ ■ φ e2 σ2 ef ★ P }} ef ?@ ⊤ {{ λ _, True }}) ⊢
-  {{ ▷ ownP σ1 ★ ▷ P }} e1 @ E {{ λ v, ∃ σ2 ef, ownP σ2 ★ ■ φ (of_val v) σ2 ef }}.
+  (∀ e2 σ2 ef, {{ ■ φ e2 σ2 ef ★ P }} ef ?@ ⊤ {{ _, True }}) ⊢
+  {{ ▷ ownP σ1 ★ ▷ P }} e1 @ E {{ v, ∃ σ2 ef, ownP σ2 ★ ■ φ (of_val v) σ2 ef }}.
 Proof.
   iIntros {? Hsafe Hstep} "#Hef".
   set (φ' e σ ef := is_Some (to_val e) ∧ φ e σ ef).
@@ -68,7 +68,7 @@ Lemma ht_lift_pure_step E (φ : expr Λ → option (expr Λ) → Prop) P P' Ψ e
   (∀ σ1, reducible e1 σ1) →
   (∀ σ1 e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → σ1 = σ2 ∧ φ e2 ef) →
   ((∀ e2 ef, {{ ■ φ e2 ef ★ P }} e2 @ E {{ Ψ }}) ∧
-   (∀ e2 ef, {{ ■ φ e2 ef ★ P' }} ef ?@ ⊤ {{ λ _, True }}))
+   (∀ e2 ef, {{ ■ φ e2 ef ★ P' }} ef ?@ ⊤ {{ _, True }}))
   ⊢ {{ ▷(P ★ P') }} e1 @ E {{ Ψ }}.
 Proof.
   iIntros {? Hsafe Hstep} "[#He2 #Hef] ! HP".
@@ -83,7 +83,7 @@ Lemma ht_lift_pure_det_step
   to_val e1 = None →
   (∀ σ1, reducible e1 σ1) →
   (∀ σ1 e2' σ2 ef', prim_step e1 σ1 e2' σ2 ef' → σ1 = σ2 ∧ e2 = e2' ∧ ef = ef')→
-  ({{ P }} e2 @ E {{ Ψ }} ∧ {{ P' }} ef ?@ ⊤ {{ λ _, True }})
+  ({{ P }} e2 @ E {{ Ψ }} ∧ {{ P' }} ef ?@ ⊤ {{ _, True }})
   ⊢ {{ ▷(P ★ P') }} e1 @ E {{ Ψ }}.
 Proof.
   iIntros {? Hsafe Hdet} "[#He2 #Hef]".
diff --git a/program_logic/invariants.v b/program_logic/invariants.v
index 490ca8baf844209bfb4bb5e426d8459f2aa718a7..da98cfd995fe82414a8a5eb9906f680ac3d61bd7 100644
--- a/program_logic/invariants.v
+++ b/program_logic/invariants.v
@@ -82,13 +82,13 @@ Proof. intros. by apply: (inv_fsa_timeless pvs_fsa). Qed.
 Lemma wp_inv E e N P Φ R :
   atomic e → nclose N ⊆ E →
   R ⊢ inv N P →
-  R ⊢ (▷ P -★ WP e @ E ∖ nclose N {{ λ v, ▷ P ★ Φ v }}) →
+  R ⊢ (▷ P -★ WP e @ E ∖ nclose N {{ v, ▷ P ★ Φ v }}) →
   R ⊢ WP e @ E {{ Φ }}.
 Proof. intros. by apply: (inv_fsa (wp_fsa e)). Qed.
 Lemma wp_inv_timeless E e N P `{!TimelessP P} Φ R :
   atomic e → nclose N ⊆ E →
   R ⊢ inv N P →
-  R ⊢ (P -★ WP e @ E ∖ nclose N {{ λ v, P ★ Φ v }}) →
+  R ⊢ (P -★ WP e @ E ∖ nclose N {{ v, P ★ Φ v }}) →
   R ⊢ WP e @ E {{ Φ }}.
 Proof. intros. by apply: (inv_fsa_timeless (wp_fsa e)). Qed.
 
diff --git a/program_logic/pviewshifts.v b/program_logic/pviewshifts.v
index 51c23f4769d970ed9bbe064baf413456aa754799..cd2ee4887ec56bcc3bfa49a88b5286945ef374c1 100644
--- a/program_logic/pviewshifts.v
+++ b/program_logic/pviewshifts.v
@@ -33,13 +33,13 @@ Arguments pvs {_ _} _ _ _%I.
 Instance: Params (@pvs) 4.
 
 Notation "|={ E1 , E2 }=> Q" := (pvs E1 E2 Q%I)
-  (at level 199, E1, E2 at level 50, Q at level 200,
+  (at level 99, E1, E2 at level 50, Q at level 200,
    format "|={ E1 , E2 }=>  Q") : uPred_scope.
 Notation "|={ E }=> Q" := (pvs E E Q%I)
-  (at level 199, E at level 50, Q at level 200,
+  (at level 99, E at level 50, Q at level 200,
    format "|={ E }=>  Q") : uPred_scope.
 Notation "|==> Q" := (pvs ⊤ ⊤ Q%I)
-  (at level 199, Q at level 200, format "|==>  Q") : uPred_scope.
+  (at level 99, Q at level 200, format "|==>  Q") : uPred_scope.
 
 Section pvs.
 Context {Λ : language} {Σ : iFunctor}.
diff --git a/program_logic/viewshifts.v b/program_logic/viewshifts.v
index eb1c9154394b614dd9723081110ec01e79ddfcb0..5bf652bac7b7c199e149c0ec6330ebceff6fd5ac 100644
--- a/program_logic/viewshifts.v
+++ b/program_logic/viewshifts.v
@@ -8,15 +8,30 @@ Definition vs {Λ Σ} (E1 E2 : coPset) (P Q : iProp Λ Σ) : iProp Λ Σ :=
 Arguments vs {_ _} _ _ _%I _%I.
 Instance: Params (@vs) 4.
 Notation "P ={ E1 , E2 }=> Q" := (vs E1 E2 P%I Q%I)
-  (at level 199, E1,E2 at level 50,
+  (at level 99, E1,E2 at level 50, Q at level 200,
    format "P  ={ E1 , E2 }=>  Q") : uPred_scope.
-Notation "P ={ E1 , E2 }=> Q" := (True ⊢ vs E1 E2 P%I Q%I)
-  (at level 199, E1, E2 at level 50,
+Notation "P ={ E1 , E2 }=> Q" := (True ⊢ (P ={E1,E2}=> Q)%I)
+  (at level 99, E1, E2 at level 50, Q at level 200,
    format "P  ={ E1 , E2 }=>  Q") : C_scope.
-Notation "P ={ E }=> Q" := (vs E E P%I Q%I)
-  (at level 199, E at level 50, format "P  ={ E }=>  Q") : uPred_scope.
-Notation "P ={ E }=> Q" := (True ⊢ vs E E P%I Q%I)
-  (at level 199, E at level 50, format "P  ={ E }=>  Q") : C_scope.
+Notation "P ={ E }=> Q" := (P ={E,E}=> Q)%I
+  (at level 99, E at level 50, Q at level 200,
+   format "P  ={ E }=>  Q") : uPred_scope.
+Notation "P ={ E }=> Q" := (True ⊢ (P ={E}=> Q)%I)
+  (at level 99, E at level 50, Q at level 200,
+   format "P  ={ E }=>  Q") : C_scope.
+
+Notation "P <={ E1 , E2 }=> Q" := ((P ={E1,E2}=> Q) ∧ (Q ={E2,E1}=> P))%I
+  (at level 99, E1,E2 at level 50, Q at level 200,
+   format "P  <={ E1 , E2 }=>  Q") : uPred_scope.
+Notation "P <={ E1 , E2 }=> Q" := (True ⊢ (P <={E1,E2}=> Q)%I)
+  (at level 99, E1, E2 at level 50, Q at level 200,
+   format "P  <={ E1 , E2 }=>  Q") : C_scope.
+Notation "P <={ E }=> Q" := (P <={E,E}=> Q)%I
+  (at level 99, E at level 50, Q at level 200,
+   format "P  <={ E }=>  Q") : uPred_scope.
+Notation "P <={ E }=> Q" := (True ⊢ (P <={E}=> Q)%I)
+  (at level 99, E at level 50, Q at level 200,
+   format "P  <={ E }=>  Q") : C_scope.
 
 Section vs.
 Context {Λ : language} {Σ : iFunctor}.
diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index fa3ec0af0e7884014ac42efa1667890726f3da86..93beb81c08013624af946a339e01037673c1b31a 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -64,6 +64,13 @@ Notation "'WP' e {{ Φ } }" := (wp ⊤ e Φ)
   (at level 20, e, Φ at level 200,
    format "'WP'  e  {{  Φ  } }") : uPred_scope.
 
+Notation "'WP' e @ E {{ v , Q } }" := (wp E e (λ v, Q))
+  (at level 20, e, Q at level 200,
+   format "'WP'  e  @  E  {{  v ,  Q  } }") : uPred_scope.
+Notation "'WP' e {{ v , Q } }" := (wp ⊤ e (λ v, Q))
+  (at level 20, e, Q at level 200,
+   format "'WP'  e  {{  v ,  Q  } }") : uPred_scope.
+
 Section wp.
 Context {Λ : language} {Σ : iFunctor}.
 Implicit Types P : iProp Λ Σ.
@@ -141,7 +148,7 @@ Proof.
   rewrite pvs_eq in Hvs. destruct (Hvs rf (S k) Ef σ1) as (r'&Hwp&?); auto.
   eapply wp_step_inv with (S k) r'; eauto.
 Qed.
-Lemma wp_pvs E e Φ : WP e @  E {{ λ v, |={E}=> Φ v }} ⊢ WP e @ E {{ Φ }}.
+Lemma wp_pvs E e Φ : WP e @  E {{ v, |={E}=> Φ v }} ⊢ WP e @ E {{ Φ }}.
 Proof.
   rewrite wp_eq. split=> n r; revert e r;
     induction n as [n IH] using lt_wf_ind=> e r Hr HΦ.
@@ -155,7 +162,7 @@ Proof.
 Qed.
 Lemma wp_atomic E1 E2 e Φ :
   E2 ⊆ E1 → atomic e →
-  (|={E1,E2}=> WP e @ E2 {{ λ v, |={E2,E1}=> Φ v }}) ⊢ WP e @ E1 {{ Φ }}.
+  (|={E1,E2}=> WP e @ E2 {{ v, |={E2,E1}=> Φ v }}) ⊢ WP e @ E1 {{ Φ }}.
 Proof.
   rewrite wp_eq pvs_eq. intros ? He; split=> n r ? Hvs; constructor.
   eauto using atomic_not_val. intros rf k Ef σ1 ???.
@@ -172,7 +179,7 @@ Proof.
   - by rewrite -assoc.
   - constructor; apply pvs_intro; auto.
 Qed.
-Lemma wp_frame_r E e Φ R : (WP e @ E {{ Φ }} ★ R) ⊢ WP e @ E {{ λ v, Φ v ★ R }}.
+Lemma wp_frame_r E e Φ R : (WP e @ E {{ Φ }} ★ R) ⊢ WP e @ E {{ v, Φ v ★ R }}.
 Proof.
   rewrite wp_eq. uPred.unseal; split; intros n r' Hvalid (r&rR&Hr&Hwp&?).
   revert Hvalid. rewrite Hr; clear Hr; revert e r Hwp.
@@ -192,8 +199,7 @@ Qed.
 Lemma wp_frame_step_r E E1 E2 e Φ R :
   to_val e = None → E ⊥ E1 → E2 ⊆ E1 →
   (WP e @ E {{ Φ }} ★ |={E1,E2}=> ▷ |={E2,E1}=> R)
-  ⊢ WP e @ (E ∪ E1) {{ λ v, Φ v ★ R }}.
-Proof.
+  ⊢ WP e @ (E ∪ E1) {{ v, Φ v ★ R }}.
   rewrite wp_eq pvs_eq=> He ??.
   uPred.unseal; split; intros n r' Hvalid (r&rR&Hr&Hwp&HR); cofe_subst.
   constructor; [done|]=>rf k Ef σ1 ?? Hws1.
@@ -222,7 +228,7 @@ Proof.
     eapply (Hmask E); by auto.
 Qed.
 Lemma wp_bind `{LanguageCtx Λ K} E e Φ :
-  WP e @ E {{ λ v, WP K (of_val v) @ E {{ Φ }} }} ⊢ WP K e @ E {{ Φ }}.
+  WP e @ E {{ v, WP K (of_val v) @ E {{ Φ }} }} ⊢ WP K e @ E {{ Φ }}.
 Proof.
   rewrite wp_eq. split=> n r; revert e r;
     induction n as [n IH] using lt_wf_ind=> e r ?.
@@ -254,10 +260,10 @@ Proof. intros; rewrite -(of_to_val e v) //; by apply wp_value'. Qed.
 Lemma wp_value_pvs E Φ e v :
   to_val e = Some v → (|={E}=> Φ v) ⊢ WP e @ E {{ Φ }}.
 Proof. intros. rewrite -wp_pvs. rewrite -wp_value //. Qed.
-Lemma wp_frame_l E e Φ R : (R ★ WP e @ E {{ Φ }}) ⊢ WP e @ E {{ λ v, R ★ Φ v }}.
+Lemma wp_frame_l E e Φ R : (R ★ WP e @ E {{ Φ }}) ⊢ WP e @ E {{ v, R ★ Φ v }}.
 Proof. setoid_rewrite (comm _ R); apply wp_frame_r. Qed.
 Lemma wp_frame_step_r' E e Φ R :
-  to_val e = None → (WP e @ E {{ Φ }} ★ ▷ R) ⊢ WP e @ E {{ λ v, Φ v ★ R }}.
+  to_val e = None → (WP e @ E {{ Φ }} ★ ▷ R) ⊢ WP e @ E {{ v, Φ v ★ R }}.
 Proof.
   intros. rewrite {2}(_ : E = E ∪ ∅); last by set_solver.
   rewrite -(wp_frame_step_r E ∅ ∅); [|auto|set_solver..].
@@ -266,22 +272,22 @@ Qed.
 Lemma wp_frame_step_l E E1 E2 e Φ R :
   to_val e = None → E ⊥ E1 → E2 ⊆ E1 →
   ((|={E1,E2}=> ▷ |={E2,E1}=> R) ★ WP e @ E {{ Φ }})
-  ⊢ WP e @ (E ∪ E1) {{ λ v, R ★ Φ v }}.
+  ⊢ WP e @ (E ∪ E1) {{ v, R ★ Φ v }}.
 Proof.
   rewrite [((|={E1,E2}=> _) ★ _)%I]comm; setoid_rewrite (comm _ R).
   apply wp_frame_step_r.
 Qed.
 Lemma wp_frame_step_l' E e Φ R :
-  to_val e = None → (▷ R ★ WP e @ E {{ Φ }}) ⊢ WP e @ E {{ λ v, R ★ Φ v }}.
+  to_val e = None → (▷ R ★ WP e @ E {{ Φ }}) ⊢ WP e @ E {{ v, R ★ Φ v }}.
 Proof.
   rewrite (comm _ (â–· R)%I); setoid_rewrite (comm _ R).
   apply wp_frame_step_r'.
 Qed.
 Lemma wp_always_l E e Φ R `{!PersistentP R} :
-  (R ∧ WP e @ E {{ Φ }}) ⊢ WP e @ E {{ λ v, R ∧ Φ v }}.
+  (R ∧ WP e @ E {{ Φ }}) ⊢ WP e @ E {{ v, R ∧ Φ v }}.
 Proof. by setoid_rewrite (always_and_sep_l _ _); rewrite wp_frame_l. Qed.
 Lemma wp_always_r E e Φ R `{!PersistentP R} :
-  (WP e @ E {{ Φ }} ∧ R) ⊢ WP e @ E {{ λ v, Φ v ∧ R }}.
+  (WP e @ E {{ Φ }} ∧ R) ⊢ WP e @ E {{ v, Φ v ∧ R }}.
 Proof. by setoid_rewrite (always_and_sep_r _ _); rewrite wp_frame_r. Qed.
 Lemma wp_wand_l E e Φ Ψ :
   ((∀ v, Φ v -★ Ψ v) ★ WP e @ E {{ Φ }}) ⊢ WP e @ E {{ Ψ }}.
diff --git a/proofmode/notation.v b/proofmode/notation.v
index 85f7a804cdf00303b019d512fc6dafba17283e41..f1c6a266342d7ba950f062b43c11f4542888e435 100644
--- a/proofmode/notation.v
+++ b/proofmode/notation.v
@@ -7,21 +7,21 @@ Arguments Enil {_}.
 Arguments Esnoc {_} _%proof_scope _%string _%uPred_scope.
 
 Notation "​" := Enil (format "​") : proof_scope.
-Notation "Γ ​ H : P" := (Esnoc Γ H P)
+Notation "​ Γ H : P" := (Esnoc Γ H P)
   (at level 1, P at level 200,
-   left associativity, format "Γ ​ '//' H  :  P") : proof_scope.
+   left associativity, format "​ Γ H  :  P '//'") : proof_scope.
 Notation "Γ '--------------------------------------' □ Δ '--------------------------------------' ★ Q" :=
   (of_envs (Envs Γ Δ) ⊢ Q%I)
   (at level 1, Q at level 200, left associativity,
-  format "Γ '//' '--------------------------------------' □ Δ '//' '--------------------------------------' ★ '//' Q '//'") :
+  format "Γ '--------------------------------------' □ '//' Δ '--------------------------------------' ★ '//' Q '//'") :
   C_scope.
 Notation "Δ '--------------------------------------' ★ Q" :=
   (of_envs (Envs Enil Δ) ⊢ Q%I)
   (at level 1, Q at level 200, left associativity,
-  format "Δ '//' '--------------------------------------' ★ '//' Q '//'") : C_scope.
+  format "Δ '--------------------------------------' ★ '//' Q '//'") : C_scope.
 Notation "Γ '--------------------------------------' □ Q" :=
   (of_envs (Envs Γ Enil) ⊢ Q%I)
   (at level 1, Q at level 200, left associativity,
-  format "Γ '//' '--------------------------------------' □ '//' Q '//'")  : C_scope.
+  format "Γ '--------------------------------------' □ '//' Q '//'")  : C_scope.
 Notation "​​ Q" := (of_envs (Envs Enil Enil) ⊢ Q%I)
-  (at level 1, format "​​ Q") : C_scope.
+  (at level 1, Q at level 200, format "​​ Q") : C_scope.
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 853b38f420c454e4a7064477dd835c55a59476a9..10a4979167fc98f5c98c5584f0322610cd83a053 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -24,7 +24,7 @@ Section LiftingTests.
   Definition heap_e  : expr [] :=
     let: "x" := ref #1 in '"x" <- !'"x" + #1 ;; !'"x".
   Lemma heap_e_spec E N :
-     nclose N ⊆ E → heap_ctx N ⊢ WP heap_e @ E {{ λ v, v = #2 }}.
+     nclose N ⊆ E → heap_ctx N ⊢ WP heap_e @ E {{ v, v = #2 }}.
   Proof.
     iIntros {HN} "#?". rewrite /heap_e. iApply (wp_mask_weaken N); first done.
     wp_alloc l as "Hl". wp_let. wp_load. wp_op. wp_store. wp_seq. by wp_load.
@@ -58,7 +58,7 @@ Section LiftingTests.
   Qed.
 
   Lemma Pred_user E :
-    (True : iProp) ⊢ WP let: "x" := Pred #42 in ^Pred '"x" @ E {{ λ v, v = #40 }}.
+    (True : iProp) ⊢ WP let: "x" := Pred #42 in ^Pred '"x" @ E {{ v, v = #40 }}.
   Proof. iIntros "". wp_apply Pred_spec. wp_let. by wp_apply Pred_spec. Qed.
 End LiftingTests.
 
@@ -66,7 +66,7 @@ Section ClosedProofs.
   Definition Σ : gFunctors := #[ heapGF ].
   Notation iProp := (iPropG heap_lang Σ).
 
-  Lemma heap_e_closed σ : {{ ownP σ : iProp }} heap_e {{ λ v, v = #2 }}.
+  Lemma heap_e_closed σ : {{ ownP σ : iProp }} heap_e {{ v, v = #2 }}.
   Proof.
     iProof. iIntros "! Hσ".
     iPvs (heap_alloc nroot) "Hσ" as {h} "[? _]"; first by rewrite nclose_nroot.
diff --git a/tests/joining_existentials.v b/tests/joining_existentials.v
index 1ac6ff266fdf4a89b1b192f8c5cd32ea28556ee5..5484081438c49120653ca88ddae5447ff91e7e7d 100644
--- a/tests/joining_existentials.v
+++ b/tests/joining_existentials.v
@@ -19,8 +19,8 @@ Definition barrier_res γ (Φ : X → iProp) : iProp :=
   (∃ x, one_shot_own γ x ★ Φ x)%I.
 
 Lemma worker_spec e γ l (Φ Ψ : X → iProp) :
-  (recv heapN N l (barrier_res γ Φ) ★ ∀ x, {{ Φ x }} e {{ λ _, Ψ x }})
-  ⊢ WP wait (%l) ;; e {{ λ _, barrier_res γ Ψ }}.
+  (recv heapN N l (barrier_res γ Φ) ★ ∀ x, {{ Φ x }} e {{ _, Ψ x }})
+  ⊢ WP wait (%l) ;; e {{ _, barrier_res γ Ψ }}.
 Proof.
   iIntros "[Hl #He]". wp_apply wait_spec; iFrame "Hl".
   iIntros "Hγ"; iDestruct "Hγ" as {x} "[#Hγ Hx]".
@@ -50,10 +50,10 @@ Qed.
 Lemma client_spec_new (eM eW1 eW2 : expr []) (eM' eW1' eW2' : expr ("b" :b: [])) :
   heapN ⊥ N → eM' = wexpr' eM → eW1' = wexpr' eW1 → eW2' = wexpr' eW2 →
   (heap_ctx heapN ★ P
-  ★ {{ P }} eM {{ λ _, ∃ x, Φ x }}
-  ★ (∀ x, {{ Φ1 x }} eW1 {{ λ _, Ψ1 x }})
-  ★ (∀ x, {{ Φ2 x }} eW2 {{ λ _, Ψ2 x }}))
-  ⊢ WP client eM' eW1' eW2' {{ λ _, ∃ γ, barrier_res γ Ψ }}.
+  ★ {{ P }} eM {{ _, ∃ x, Φ x }}
+  ★ (∀ x, {{ Φ1 x }} eW1 {{ _, Ψ1 x }})
+  ★ (∀ x, {{ Φ2 x }} eW2 {{ _, Ψ2 x }}))
+  ⊢ WP client eM' eW1' eW2' {{ _, ∃ γ, barrier_res γ Ψ }}.
 Proof.
   iIntros {HN -> -> ->} "/= (#Hh&HP&#He&#He1&#He2)"; rewrite /client.
   iPvs one_shot_alloc as {γ} "Hγ".
diff --git a/tests/one_shot.v b/tests/one_shot.v
index 5134a793c403618d25c7dac07ec2aea60bde7c24..3546f8bd743567953eec1b97e0cfdf0a49c18ddf 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -37,8 +37,8 @@ Definition one_shot_inv (γ : gname) (l : loc) : iProp :=
 
 Lemma wp_one_shot (Φ : val → iProp) :
   (heap_ctx heapN ★ ∀ f1 f2 : val,
-    (∀ n : Z, □ WP f1 #n {{ λ w, w = #true ∨ w = #false }}) ★
-    □ WP f2 #() {{ λ g, □ WP g #() {{ λ _, True }} }} -★ Φ (f1,f2)%V)
+    (∀ n : Z, □ WP f1 #n {{ w, w = #true ∨ w = #false }}) ★
+    □ WP f2 #() {{ g, □ WP g #() {{ _, True }} }} -★ Φ (f1,f2)%V)
   ⊢ WP one_shot_example #() {{ Φ }}.
 Proof.
   iIntros "[#? Hf] /=".
@@ -83,9 +83,9 @@ Qed.
 
 Lemma hoare_one_shot (Φ : val → iProp) :
   heap_ctx heapN ⊢ {{ True }} one_shot_example #()
-    {{ λ ff,
-      (∀ n : Z, {{ True }} Fst ff #n {{ λ w, w = #true ∨ w = #false }}) ★
-      {{ True }} Snd ff #() {{ λ g, {{ True }} g #() {{ λ _, True }} }}
+    {{ ff,
+      (∀ n : Z, {{ True }} Fst ff #n {{ w, w = #true ∨ w = #false }}) ★
+      {{ True }} Snd ff #() {{ g, {{ True }} g #() {{ _, True }} }}
     }}.
 Proof.
   iIntros "#? ! _". iApply wp_one_shot. iSplit; first done.