diff --git a/barrier/barrier.v b/barrier/barrier.v
index 9e74643641611e9d2ecbce55b2c3378c68772cf5..4a8c73a19f5bf328b011c9c5e72e67332a273e85 100644
--- a/barrier/barrier.v
+++ b/barrier/barrier.v
@@ -146,7 +146,7 @@ Section proof.
 
   Lemma newchan_spec (P : iProp) (Φ : val → iProp) :
     (heap_ctx heapN ★ ∀ l, recv l P ★ send l P -★ Φ (LocV l))
-    ⊑ wp ⊤ (newchan '()) Φ.
+    ⊑ || newchan '() {{ Φ }}.
   Proof.
     rewrite /newchan. wp_rec. (* TODO: wp_seq. *)
     rewrite -wp_pvs. wp> eapply wp_alloc; eauto with I ndisj.
@@ -196,7 +196,7 @@ Section proof.
   Qed.
 
   Lemma signal_spec l P (Φ : val → iProp) :
-    heapN ⊥ N → (send l P ★ P ★ Φ '()) ⊑ wp ⊤ (signal (LocV l)) Φ.
+    heapN ⊥ N → (send l P ★ P ★ Φ '()) ⊑ || signal (LocV l) {{ Φ }}.
   Proof.
     intros Hdisj. rewrite /signal /send /barrier_ctx. rewrite sep_exist_r.
     apply exist_elim=>γ. wp_rec. (* FIXME wp_let *)
@@ -226,12 +226,12 @@ Section proof.
   Qed.
 
   Lemma wait_spec l P (Φ : val → iProp) :
-    heapN ⊥ N → (recv l P ★ (P -★ Φ '())) ⊑ wp ⊤ (wait (LocV l)) Φ.
+    heapN ⊥ N → (recv l P ★ (P -★ Φ '())) ⊑ || wait (LocV l) {{ Φ }}.
   Proof.
   Abort.
 
   Lemma split_spec l P1 P2 Φ :
-    (recv l (P1 ★ P2) ★ (recv l P1 ★ recv l P2 -★ Φ '())) ⊑ wp ⊤ Skip Φ.
+    (recv l (P1 ★ P2) ★ (recv l P1 ★ recv l P2 -★ Φ '())) ⊑ || Skip {{ Φ }}.
   Proof.
   Abort.
 
diff --git a/heap_lang/derived.v b/heap_lang/derived.v
index 202e9f9734ed1982903e81b47b2146072847035f..033dd3df09d48e117770cf0ac7493206a561f58f 100644
--- a/heap_lang/derived.v
+++ b/heap_lang/derived.v
@@ -17,44 +17,47 @@ Implicit Types Φ : val → iProp heap_lang Σ.
 
 (** Proof rules for the sugar *)
 Lemma wp_lam' E x ef e v Φ :
-  to_val e = Some v → ▷ wp E (subst ef x v) Φ ⊑ wp E (App (Lam x ef) e) Φ.
+  to_val e = Some v →
+  ▷ || subst ef x v @ E {{ Φ }} ⊑ || App (Lam x ef) e @ E {{ Φ }}.
 Proof. intros. by rewrite -wp_rec' ?subst_empty. Qed.
 
 Lemma wp_let' E x e1 e2 v Φ :
-  to_val e1 = Some v → ▷ wp E (subst e2 x v) Φ ⊑ wp E (Let x e1 e2) Φ.
+  to_val e1 = Some v →
+  ▷ || subst e2 x v @ E {{ Φ }} ⊑ || Let x e1 e2 @ E {{ Φ }}.
 Proof. apply wp_lam'. Qed.
 
-Lemma wp_seq E e1 e2 Φ : wp E e1 (λ _, ▷ wp E e2 Φ) ⊑ wp E (Seq e1 e2) Φ.
+Lemma wp_seq E e1 e2 Φ :
+  || e1 @ E {{ λ _, ▷ || e2 @ E {{ Φ }} }} ⊑ || Seq e1 e2 @ E {{ Φ }}.
 Proof.
   rewrite -(wp_bind [LetCtx "" e2]). apply wp_mono=>v.
   by rewrite -wp_let' //= ?to_of_val ?subst_empty.
 Qed.
 
-Lemma wp_skip E Φ : ▷ (Φ (LitV LitUnit)) ⊑ wp E Skip Φ.
+Lemma wp_skip E Φ : ▷ Φ (LitV LitUnit) ⊑ || Skip @ E {{ Φ }}.
 Proof. rewrite -wp_seq -wp_value // -wp_value //. Qed.
 
 Lemma wp_le E (n1 n2 : Z) P Φ :
-  (n1 ≤ n2 → P ⊑ ▷ Φ (LitV $ LitBool true)) →
-  (n2 < n1 → P ⊑ ▷ Φ (LitV $ LitBool false)) →
-  P ⊑ wp E (BinOp LeOp (Lit $ LitInt n1) (Lit $ LitInt n2)) Φ.
+  (n1 ≤ n2 → P ⊑ ▷ Φ (LitV (LitBool true))) →
+  (n2 < n1 → P ⊑ ▷ Φ (LitV (LitBool false))) →
+  P ⊑ || BinOp LeOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}.
 Proof.
   intros. rewrite -wp_bin_op //; [].
   destruct (bool_decide_reflect (n1 ≤ n2)); by eauto with omega.
 Qed.
 
 Lemma wp_lt E (n1 n2 : Z) P Φ :
-  (n1 < n2 → P ⊑ ▷ Φ (LitV $ LitBool true)) →
-  (n2 ≤ n1 → P ⊑ ▷ Φ (LitV $ LitBool false)) →
-  P ⊑ wp E (BinOp LtOp (Lit $ LitInt n1) (Lit $ LitInt n2)) Φ.
+  (n1 < n2 → P ⊑ ▷ Φ (LitV (LitBool true))) →
+  (n2 ≤ n1 → P ⊑ ▷ Φ (LitV (LitBool false))) →
+  P ⊑ || BinOp LtOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}.
 Proof.
   intros. rewrite -wp_bin_op //; [].
   destruct (bool_decide_reflect (n1 < n2)); by eauto with omega.
 Qed.
 
 Lemma wp_eq E (n1 n2 : Z) P Φ :
-  (n1 = n2 → P ⊑ ▷ Φ (LitV $ LitBool true)) →
-  (n1 ≠ n2 → P ⊑ ▷ Φ (LitV $ LitBool false)) →
-  P ⊑ wp E (BinOp EqOp (Lit $ LitInt n1) (Lit $ LitInt n2)) Φ.
+  (n1 = n2 → P ⊑ ▷ Φ (LitV (LitBool true))) →
+  (n1 ≠ n2 → P ⊑ ▷ Φ (LitV (LitBool false))) →
+  P ⊑ || BinOp EqOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}.
 Proof.
   intros. rewrite -wp_bin_op //; [].
   destruct (bool_decide_reflect (n1 = n2)); by eauto with omega.
diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index b11be3557f2dc7d1bf0907447aae4d66c5105be8..69596f9b642d3e81f5c2969f44b63f3eb5dede0e 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -65,7 +65,7 @@ Section heap.
   (** Allocation *)
   Lemma heap_alloc E N σ :
     authG heap_lang Σ heapRA → nclose N ⊆ E →
-    ownP σ ⊑ (|={E}=> ∃ (_ : heapG Σ), heap_ctx N ∧ Π★{map σ} heap_mapsto).
+    ownP σ ⊑ (|={E}=> ∃ _ : heapG Σ, heap_ctx N ∧ Π★{map σ} heap_mapsto).
   Proof.
     intros. rewrite -{1}(from_to_heap σ). etransitivity.
     { rewrite [ownP _]later_intro.
@@ -100,7 +100,7 @@ Section heap.
     to_val e = Some v → nclose N ⊆ E →
     P ⊑ heap_ctx N →
     P ⊑ (▷ ∀ l, l ↦ v -★ Φ (LocV l)) →
-    P ⊑ wp E (Alloc e) Φ.
+    P ⊑ || Alloc e @ E {{ Φ }}.
   Proof.
     rewrite /heap_ctx /heap_inv /heap_mapsto=> ?? Hctx HP.
     transitivity (|={E}=> auth_own heap_name ∅ ★ P)%I.
@@ -127,7 +127,7 @@ Section heap.
     nclose N ⊆ E →
     P ⊑ heap_ctx N →
     P ⊑ (▷ l ↦ v ★ ▷ (l ↦ v -★ Φ v)) →
-    P ⊑ wp E (Load (Loc l)) Φ.
+    P ⊑ || Load (Loc l) @ E {{ Φ }}.
   Proof.
     rewrite /heap_ctx /heap_inv /heap_mapsto=>HN ? HPΦ.
     apply (auth_fsa' heap_inv (wp_fsa _) id)
@@ -146,7 +146,7 @@ Section heap.
     to_val e = Some v → nclose N ⊆ E → 
     P ⊑ heap_ctx N →
     P ⊑ (▷ l ↦ v' ★ ▷ (l ↦ v -★ Φ (LitV LitUnit))) →
-    P ⊑ wp E (Store (Loc l) e) Φ.
+    P ⊑ || Store (Loc l) e @ E {{ Φ }}.
   Proof.
     rewrite /heap_ctx /heap_inv /heap_mapsto=>? HN ? HPΦ.
     apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Excl v) l))
@@ -167,7 +167,7 @@ Section heap.
     nclose N ⊆ E →
     P ⊑ heap_ctx N →
     P ⊑ (▷ l ↦ v' ★ ▷ (l ↦ v' -★ Φ (LitV (LitBool false)))) →
-    P ⊑ wp E (Cas (Loc l) e1 e2) Φ.
+    P ⊑ || Cas (Loc l) e1 e2 @ E {{ Φ }}.
   Proof.
     rewrite /heap_ctx /heap_inv /heap_mapsto=>??? HN ? HPΦ.
     apply (auth_fsa' heap_inv (wp_fsa _) id)
@@ -187,7 +187,7 @@ Section heap.
     nclose N ⊆ E →
     P ⊑ heap_ctx N →
     P ⊑ (▷ l ↦ v1 ★ ▷ (l ↦ v2 -★ Φ (LitV (LitBool true)))) →
-    P ⊑ wp E (Cas (Loc l) e1 e2) Φ.
+    P ⊑ || Cas (Loc l) e1 e2 @ E {{ Φ }}.
   Proof.
     rewrite /heap_ctx /heap_inv /heap_mapsto=> ?? HN ? HPΦ.
     apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Excl v2) l))
diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v
index 4fd62284b40503dc397b6ee0eb2818d6188dbb5a..5359b62ba1a0990e528c9c4e7e4a4836710291ae 100644
--- a/heap_lang/lifting.v
+++ b/heap_lang/lifting.v
@@ -16,18 +16,14 @@ Implicit Types ef : option expr.
 
 (** Bind. *)
 Lemma wp_bind {E e} K Φ :
-  wp E e (λ v, wp E (fill K (of_val v)) Φ) ⊑ wp E (fill K e) Φ.
-Proof. apply weakestpre.wp_bind. Qed.
-
-Lemma wp_bindi {E e} Ki Φ :
-  wp E e (λ v, wp E (fill_item Ki (of_val v)) Φ) ⊑ wp E (fill_item Ki e) Φ.
+  || e @ E {{ λ v, || fill K (of_val v) @ E {{ Φ }}}} ⊑ || fill K e @ E {{ Φ }}.
 Proof. apply weakestpre.wp_bind. Qed.
 
 (** Base axioms for core primitives of the language: Stateful reductions. *)
 Lemma wp_alloc_pst E σ e v Φ :
   to_val e = Some v →
   (ownP σ ★ ▷ (∀ l, σ !! l = None ∧ ownP (<[l:=v]>σ) -★ Φ (LocV l)))
-       ⊑ wp E (Alloc e) Φ.
+  ⊑ || Alloc e @ E {{ Φ }}.
 Proof.
   (* TODO RJ: This works around ssreflect bug #22. *)
   intros. set (φ v' σ' ef := ∃ l,
@@ -44,7 +40,7 @@ Qed.
 
 Lemma wp_load_pst E σ l v Φ :
   σ !! l = Some v →
-  (ownP σ ★ ▷ (ownP σ -★ Φ v)) ⊑ wp E (Load (Loc l)) Φ.
+  (ownP σ ★ ▷ (ownP σ -★ Φ v)) ⊑ || Load (Loc l) @ E {{ Φ }}.
 Proof.
   intros. rewrite -(wp_lift_atomic_det_step σ v σ None) ?right_id //;
     last by intros; inv_step; eauto using to_of_val.
@@ -52,7 +48,8 @@ Qed.
 
 Lemma wp_store_pst E σ l e v v' Φ :
   to_val e = Some v → σ !! l = Some v' →
-  (ownP σ ★ ▷ (ownP (<[l:=v]>σ) -★ Φ (LitV LitUnit))) ⊑ wp E (Store (Loc l) e) Φ.
+  (ownP σ ★ ▷ (ownP (<[l:=v]>σ) -★ Φ (LitV LitUnit)))
+  ⊑ || Store (Loc l) e @ E {{ Φ }}.
 Proof.
   intros. rewrite -(wp_lift_atomic_det_step σ (LitV LitUnit) (<[l:=v]>σ) None)
     ?right_id //; last by intros; inv_step; eauto.
@@ -60,7 +57,8 @@ Qed.
 
 Lemma wp_cas_fail_pst E σ l e1 v1 e2 v2 v' Φ :
   to_val e1 = Some v1 → to_val e2 = Some v2 → σ !! l = Some v' → v' ≠ v1 →
-  (ownP σ ★ ▷ (ownP σ -★ Φ (LitV $ LitBool false))) ⊑ wp E (Cas (Loc l) e1 e2) Φ.
+  (ownP σ ★ ▷ (ownP σ -★ Φ (LitV $ LitBool false)))
+  ⊑ || Cas (Loc l) e1 e2 @ E {{ Φ }}.
 Proof.
   intros. rewrite -(wp_lift_atomic_det_step σ (LitV $ LitBool false) σ None)
     ?right_id //; last by intros; inv_step; eauto.
@@ -69,15 +67,15 @@ Qed.
 Lemma wp_cas_suc_pst E σ l e1 v1 e2 v2 Φ :
   to_val e1 = Some v1 → to_val e2 = Some v2 → σ !! l = Some v1 →
   (ownP σ ★ ▷ (ownP (<[l:=v2]>σ) -★ Φ (LitV $ LitBool true)))
-  ⊑ wp E (Cas (Loc l) e1 e2) Φ.
+  ⊑ || Cas (Loc l) e1 e2 @ E {{ Φ }}.
 Proof.
-  intros. rewrite -(wp_lift_atomic_det_step σ (LitV $ LitBool true) (<[l:=v2]>σ) None)
-    ?right_id //; last by intros; inv_step; eauto.
+  intros. rewrite -(wp_lift_atomic_det_step σ (LitV $ LitBool true)
+    (<[l:=v2]>σ) None) ?right_id //; last by intros; inv_step; eauto.
 Qed.
 
 (** Base axioms for core primitives of the language: Stateless reductions *)
 Lemma wp_fork E e Φ :
-  (▷ Φ (LitV LitUnit) ★ ▷ wp (Σ:=Σ) ⊤ e (λ _, True)) ⊑ wp E (Fork e) Φ.
+  (▷ Φ (LitV LitUnit) ★ ▷ || e {{ λ _, True }}) ⊑ || Fork e @ E {{ Φ }}.
 Proof.
   rewrite -(wp_lift_pure_det_step (Fork e) (Lit LitUnit) (Some e)) //=;
     last by intros; inv_step; eauto.
@@ -88,7 +86,8 @@ Qed.
    The final version is defined in substitution.v. *)
 Lemma wp_rec' E f x e1 e2 v Φ :
   to_val e2 = Some v →
-  ▷ wp E (subst (subst e1 f (RecV f x e1)) x v) Φ ⊑ wp E (App (Rec f x e1) e2) Φ.
+  ▷ || subst (subst e1 f (RecV f x e1)) x v @ E {{ Φ }}
+  ⊑ || App (Rec f x e1) e2 @ E {{ Φ }}.
 Proof.
   intros. rewrite -(wp_lift_pure_det_step (App _ _)
     (subst (subst e1 f (RecV f x e1)) x v) None) ?right_id //=;
@@ -97,7 +96,7 @@ Qed.
 
 Lemma wp_un_op E op l l' Φ :
   un_op_eval op l = Some l' →
-  ▷ Φ (LitV l') ⊑ wp E (UnOp op (Lit l)) Φ.
+  ▷ Φ (LitV l') ⊑ || UnOp op (Lit l) @ E {{ Φ }}.
 Proof.
   intros. rewrite -(wp_lift_pure_det_step (UnOp op _) (Lit l') None)
     ?right_id -?wp_value //; intros; inv_step; eauto.
@@ -105,21 +104,21 @@ Qed.
 
 Lemma wp_bin_op E op l1 l2 l' Φ :
   bin_op_eval op l1 l2 = Some l' →
-  ▷ Φ (LitV l') ⊑ wp E (BinOp op (Lit l1) (Lit l2)) Φ.
+  ▷ Φ (LitV l') ⊑ || BinOp op (Lit l1) (Lit l2) @ E {{ Φ }}.
 Proof.
   intros Heval. rewrite -(wp_lift_pure_det_step (BinOp op _ _) (Lit l') None)
     ?right_id -?wp_value //; intros; inv_step; eauto.
 Qed.
 
 Lemma wp_if_true E e1 e2 Φ :
-  ▷ wp E e1 Φ ⊑ wp E (If (Lit $ LitBool true) e1 e2) Φ.
+  ▷ || e1 @ E {{ Φ }} ⊑ || If (Lit (LitBool true)) e1 e2 @ E {{ Φ }}.
 Proof.
   rewrite -(wp_lift_pure_det_step (If _ _ _) e1 None)
     ?right_id //; intros; inv_step; eauto.
 Qed.
 
 Lemma wp_if_false E e1 e2 Φ :
-  ▷ wp E e2 Φ ⊑ wp E (If (Lit $ LitBool false) e1 e2) Φ.
+  ▷ || e2 @ E {{ Φ }} ⊑ || If (Lit (LitBool false)) e1 e2 @ E {{ Φ }}.
 Proof.
   rewrite -(wp_lift_pure_det_step (If _ _ _) e2 None)
     ?right_id //; intros; inv_step; eauto.
@@ -127,7 +126,7 @@ Qed.
 
 Lemma wp_fst E e1 v1 e2 v2 Φ :
   to_val e1 = Some v1 → to_val e2 = Some v2 →
-  ▷ Φ v1 ⊑ wp E (Fst $ Pair e1 e2) Φ.
+  ▷ Φ v1 ⊑ || Fst (Pair e1 e2) @ E {{ Φ }}.
 Proof.
   intros. rewrite -(wp_lift_pure_det_step (Fst _) e1 None)
     ?right_id -?wp_value //; intros; inv_step; eauto.
@@ -135,7 +134,7 @@ Qed.
 
 Lemma wp_snd E e1 v1 e2 v2 Φ :
   to_val e1 = Some v1 → to_val e2 = Some v2 →
-  ▷ Φ v2 ⊑ wp E (Snd $ Pair e1 e2) Φ.
+  ▷ Φ v2 ⊑ || Snd (Pair e1 e2) @ E {{ Φ }}.
 Proof.
   intros. rewrite -(wp_lift_pure_det_step (Snd _) e2 None)
     ?right_id -?wp_value //; intros; inv_step; eauto.
@@ -143,7 +142,7 @@ Qed.
 
 Lemma wp_case_inl' E e0 v0 x1 e1 x2 e2 Φ :
   to_val e0 = Some v0 →
-  ▷ wp E (subst e1 x1 v0) Φ ⊑ wp E (Case (InjL e0) x1 e1 x2 e2) Φ.
+  ▷ || subst e1 x1 v0 @ E {{ Φ }} ⊑ || Case (InjL e0) x1 e1 x2 e2 @ E {{ Φ }}.
 Proof.
   intros. rewrite -(wp_lift_pure_det_step (Case _ _ _ _ _)
     (subst e1 x1 v0) None) ?right_id //; intros; inv_step; eauto.
@@ -151,7 +150,7 @@ Qed.
 
 Lemma wp_case_inr' E e0 v0 x1 e1 x2 e2 Φ :
   to_val e0 = Some v0 →
-  ▷ wp E (subst e2 x2 v0) Φ ⊑ wp E (Case (InjR e0) x1 e1 x2 e2) Φ.
+  ▷ || subst e2 x2 v0 @ E {{ Φ }} ⊑ || Case (InjR e0) x1 e1 x2 e2 @ E {{ Φ }}.
 Proof.
   intros. rewrite -(wp_lift_pure_det_step (Case _ _ _ _ _)
     (subst e2 x2 v0) None) ?right_id //; intros; inv_step; eauto.
diff --git a/heap_lang/notation.v b/heap_lang/notation.v
index 30db88cc834be2eaabc7111e9e3a534d5943b41c..0361e80221277a83521eee7b2c1fed5af6c4cb77 100644
--- a/heap_lang/notation.v
+++ b/heap_lang/notation.v
@@ -1,7 +1,12 @@
 From heap_lang Require Export derived.
 
-(* What about Arguments for hoare triples?. *)
 Arguments wp {_ _} _ _%L _.
+Notation "|| e @ E {{ Φ } }" := (wp E e%L Φ)
+  (at level 20, e, Φ at level 200,
+   format "||  e  @  E  {{  Φ  } }") : uPred_scope.
+Notation "|| e {{ Φ } }" := (wp ⊤ e%L Φ)
+  (at level 20, e, Φ at level 200,
+   format "||  e   {{  Φ  } }") : uPred_scope.
 
 Coercion LitInt : Z >-> base_lit.
 Coercion LitBool : bool >-> base_lit.
diff --git a/heap_lang/substitution.v b/heap_lang/substitution.v
index 4ea9afc6f887d71810032b7d714fb24807a57792..cd44917e790abf9af115c6ba64951431ca4d6592 100644
--- a/heap_lang/substitution.v
+++ b/heap_lang/substitution.v
@@ -26,10 +26,10 @@ to be unfolded. For example, consider the rule [wp_rec'] from below:
 <<
   Definition foo : val := rec: "f" "x" := ... .
 
-  Lemma wp_rec' E e1 f x erec e2 v Q :
+  Lemma wp_rec E e1 f x erec e2 v Φ :
     e1 = Rec f x erec →
     to_val e2 = Some v →
-    ▷ wp E (gsubst (gsubst erec f e1) x e2) Q ⊑ wp E (App e1 e2) Q.
+    ▷ || gsubst (gsubst erec f e1) x e2 @ E {{ Φ }} ⊑ || App e1 e2 @ E {{ Φ }}.
 >>
 
 We ensure that [e1] is substituted instead of [RecV f x erec]. So, for example
@@ -123,7 +123,7 @@ Hint Resolve to_of_val.
 Lemma wp_rec E e1 f x erec e2 v Φ :
   e1 = Rec f x erec →
   to_val e2 = Some v →
-  ▷ wp E (gsubst (gsubst erec f e1) x e2) Φ ⊑ wp E (App e1 e2) Φ.
+  ▷ || gsubst (gsubst erec f e1) x e2 @ E {{ Φ }} ⊑ || App e1 e2 @ E {{ Φ }}.
 Proof.
   intros -> <-%of_to_val.
   rewrite (gsubst_correct _ _ (RecV _ _ _)) gsubst_correct.
@@ -131,21 +131,22 @@ Proof.
 Qed.
 
 Lemma wp_lam E x ef e v Φ :
-  to_val e = Some v → ▷ wp E (gsubst ef x e) Φ ⊑ wp E (App (Lam x ef) e) Φ.
+  to_val e = Some v →
+  ▷ || gsubst ef x e @ E {{ Φ }} ⊑ || App (Lam x ef) e @ E {{ Φ }}.
 Proof. intros <-%of_to_val; rewrite gsubst_correct. by apply wp_lam'. Qed.
 
 Lemma wp_let E x e1 e2 v Φ :
-  to_val e1 = Some v → ▷ wp E (gsubst e2 x e1) Φ ⊑ wp E (Let x e1 e2) Φ.
+  to_val e1 = Some v →
+  ▷ || gsubst e2 x e1 @ E {{ Φ }} ⊑ || Let x e1 e2 @ E {{ Φ }}.
 Proof. apply wp_lam. Qed.
 
 Lemma wp_case_inl E e0 v0 x1 e1 x2 e2 Φ :
   to_val e0 = Some v0 →
-  ▷ wp E (gsubst e1 x1 e0) Φ ⊑ wp E (Case (InjL e0) x1 e1 x2 e2) Φ.
+  ▷ || gsubst e1 x1 e0 @ E {{ Φ }} ⊑ || Case (InjL e0) x1 e1 x2 e2 @ E {{ Φ }}.
 Proof. intros <-%of_to_val; rewrite gsubst_correct. by apply wp_case_inl'. Qed.
 
 Lemma wp_case_inr E e0 v0 x1 e1 x2 e2 Φ :
   to_val e0 = Some v0 →
-  ▷ wp E (gsubst e2 x2 e0) Φ ⊑ wp E (Case (InjR e0) x1 e1 x2 e2) Φ.
+  ▷ || gsubst e2 x2 e0 @ E {{ Φ }} ⊑ || Case (InjR e0) x1 e1 x2 e2 @ E {{ Φ }}.
 Proof. intros <-%of_to_val; rewrite gsubst_correct. by apply wp_case_inr'. Qed.
 End wp.
-
diff --git a/heap_lang/tests.v b/heap_lang/tests.v
index 973c42488085fe41a8871f892a169b24549f21ee..34b146d677c0a51e48c6634cd27f29ca1e648962 100644
--- a/heap_lang/tests.v
+++ b/heap_lang/tests.v
@@ -29,7 +29,8 @@ 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 E heap_e (λ v, v = '2).
+  Lemma heap_e_spec E N :
+     nclose N ⊆ E → heap_ctx N ⊑ || heap_e @ E {{ λ v, v = '2 }}.
   Proof.
     rewrite /heap_e=>HN. rewrite -(wp_mask_weaken N E) //.
     wp> eapply wp_alloc; eauto. apply forall_intro=>l; apply wand_intro_l.
@@ -48,7 +49,7 @@ Section LiftingTests.
       if: "x" ≤ '0 then -FindPred (-"x" + '2) '0 else FindPred "x" '0.
 
   Lemma FindPred_spec n1 n2 E Φ :
-    (■ (n1 < n2) ∧ Φ '(n2 - 1)) ⊑ wp E (FindPred 'n2 'n1) Φ.
+    (■ (n1 < n2) ∧ Φ '(n2 - 1)) ⊑ || FindPred 'n2 'n1 @ E {{ Φ }}.
   Proof.
     revert n1; apply löb_all_1=>n1.
     rewrite (comm uPred_and (â–  _)%I) assoc; apply const_elim_r=>?.
@@ -62,7 +63,7 @@ Section LiftingTests.
     - wp_value. assert (n1 = n2 - 1) as -> by omega; auto with I.
   Qed.
 
-  Lemma Pred_spec n E Φ : ▷ Φ (LitV (n - 1)) ⊑ wp E (Pred 'n)%L Φ.
+  Lemma Pred_spec n E Φ : ▷ Φ (LitV (n - 1)) ⊑ || Pred 'n @ E {{ Φ }}.
   Proof.
     wp_rec>; apply later_mono; wp_bin_op=> ?; wp_if.
     - wp_un_op. wp_bin_op.
@@ -73,7 +74,7 @@ Section LiftingTests.
   Qed.
 
   Lemma Pred_user E :
-    True ⊑ wp (Σ:=globalF Σ) E (let: "x" := Pred '42 in Pred "x") (λ v, v = '40).
+    (True : iProp) ⊑ || let: "x" := Pred '42 in Pred "x" @ E {{ λ v, v = '40 }}.
   Proof.
     intros. ewp> apply Pred_spec. wp_rec. ewp> apply Pred_spec. auto with I.
   Qed.
diff --git a/program_logic/hoare.v b/program_logic/hoare.v
index 116c9da53b81fb774b02c70635255c962793463e..643f92e9c618e49def2e2a8922e9a65f1f51c2b5 100644
--- a/program_logic/hoare.v
+++ b/program_logic/hoare.v
@@ -1,7 +1,8 @@
 From program_logic Require Export weakestpre viewshifts.
 
 Definition ht {Λ Σ} (E : coPset) (P : iProp Λ Σ)
-  (e : expr Λ) (Φ : val Λ → iProp Λ Σ) : iProp Λ Σ := (□ (P → wp E e Φ))%I.
+    (e : expr Λ) (Φ : val Λ → iProp Λ Σ) : iProp Λ Σ :=
+  (□ (P → || e @ E {{ Φ }}))%I.
 Instance: Params (@ht) 3.
 
 Notation "{{ P } } e @ E {{ Φ } }" := (ht E P e Φ)
@@ -37,7 +38,7 @@ Global Instance ht_mono' E :
   Proper (flip (⊑) ==> eq ==> pointwise_relation _ (⊑) ==> (⊑)) (@ht Λ Σ E).
 Proof. by intros P P' HP e ? <- Φ Φ' HΦ; apply ht_mono. Qed.
 
-Lemma ht_alt E P Φ e : (P ⊑ wp E e Φ) → {{ P }} e @ E {{ Φ }}.
+Lemma ht_alt E P Φ e : (P ⊑ || e @ E {{ Φ }}) → {{ P }} e @ E {{ Φ }}.
 Proof.
   intros; rewrite -{1}always_const. apply: always_intro. apply impl_intro_l.
   by rewrite always_const right_id.
diff --git a/program_logic/invariants.v b/program_logic/invariants.v
index 4a5febf57b0674e783e285d7d79abb1cbd335af9..b9dcdea18836e8fb5b42fd35588befeb1ebd4391 100644
--- a/program_logic/invariants.v
+++ b/program_logic/invariants.v
@@ -64,8 +64,8 @@ Proof. intros. by apply: (inv_fsa pvs_fsa). Qed.
 Lemma wp_open_close E e N P Φ R :
   atomic e → nclose N ⊆ E →
   R ⊑ inv N P →
-  R ⊑ (▷ P -★ wp (E ∖ nclose N) e (λ v, ▷ P ★ Φ v)) →
-  R ⊑ wp E e Φ.
+  R ⊑ (▷ P -★ || e @ E ∖ nclose N {{ λ v, ▷ P ★ Φ v }}) →
+  R ⊑ || e @ E {{ Φ }}.
 Proof. intros. by apply: (inv_fsa (wp_fsa e)). Qed.
 
 Lemma inv_alloc N P : ▷ P ⊑ pvs N N (inv N P).
diff --git a/program_logic/lifting.v b/program_logic/lifting.v
index 93f4cf9ded3f8924ae651bb09334b2f0eff77838..77cd393d0259e98ada8f51bfeec4be4fc6e0648d 100644
--- a/program_logic/lifting.v
+++ b/program_logic/lifting.v
@@ -24,8 +24,8 @@ Lemma wp_lift_step E1 E2
   reducible e1 σ1 →
   (∀ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → φ e2 σ2 ef) →
   (|={E2,E1}=> ownP σ1 ★ ▷ ∀ e2 σ2 ef,
-    (■ φ e2 σ2 ef ∧ ownP σ2) -★ |={E1,E2}=> wp E2 e2 Φ ★ wp_fork ef)
-  ⊑ wp E2 e1 Φ.
+    (■ φ e2 σ2 ef ∧ ownP σ2) -★ |={E1,E2}=> || e2 @ E2 {{ Φ }} ★ wp_fork ef)
+  ⊑ || e1 @ E2 {{ Φ }}.
 Proof.
   intros ? He Hsafe Hstep n r ? Hvs; constructor; auto.
   intros rf k Ef σ1' ???; destruct (Hvs rf (S k) Ef σ1')
@@ -45,7 +45,7 @@ Lemma wp_lift_pure_step E (φ : expr Λ → option (expr Λ) → Prop) Φ e1 :
   to_val e1 = None →
   (∀ σ1, reducible e1 σ1) →
   (∀ σ1 e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → σ1 = σ2 ∧ φ e2 ef) →
-  (▷ ∀ e2 ef, ■ φ e2 ef → wp E e2 Φ ★ wp_fork ef) ⊑ wp E e1 Φ.
+  (▷ ∀ e2 ef, ■ φ e2 ef → || e2 @ E {{ Φ }} ★ wp_fork ef) ⊑ || e1 @ E {{ Φ }}.
 Proof.
   intros He Hsafe Hstep n r ? Hwp; constructor; auto.
   intros rf k Ef σ1 ???; split; [done|]. destruct n as [|n]; first lia.
@@ -65,7 +65,7 @@ Lemma wp_lift_atomic_step {E Φ} e1
   (∀ e2 σ2 ef,
     prim_step e1 σ1 e2 σ2 ef → ∃ v2, to_val e2 = Some v2 ∧ φ v2 σ2 ef) →
   (ownP σ1 ★ ▷ ∀ v2 σ2 ef, ■ φ v2 σ2 ef ∧ ownP σ2 -★ Φ v2 ★ wp_fork ef)
-  ⊑ wp E e1 Φ.
+  ⊑ || e1 @ E {{ Φ }}.
 Proof.
   intros. rewrite -(wp_lift_step E E (λ e2 σ2 ef, ∃ v2,
     to_val e2 = Some v2 ∧ φ v2 σ2 ef) _ e1 σ1) //; [].
@@ -84,7 +84,7 @@ Lemma wp_lift_atomic_det_step {E Φ e1} σ1 v2 σ2 ef :
   reducible e1 σ1 →
   (∀ e2' σ2' ef', prim_step e1 σ1 e2' σ2' ef' →
     σ2 = σ2' ∧ to_val e2' = Some v2 ∧ ef = ef') →
-  (ownP σ1 ★ ▷ (ownP σ2 -★ Φ v2 ★ wp_fork ef)) ⊑ wp E e1 Φ.
+  (ownP σ1 ★ ▷ (ownP σ2 -★ Φ v2 ★ wp_fork ef)) ⊑ || e1 @ E {{ Φ }}.
 Proof.
   intros. rewrite -(wp_lift_atomic_step _ (λ v2' σ2' ef',
     σ2 = σ2' ∧ v2 = v2' ∧ ef = ef') σ1) //; last naive_solver.
@@ -99,7 +99,7 @@ Lemma wp_lift_pure_det_step {E Φ} e1 e2 ef :
   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')→
-  ▷ (wp E e2 Φ ★ wp_fork ef) ⊑ wp E e1 Φ.
+  ▷ (|| e2 @ E {{ Φ }} ★ wp_fork ef) ⊑ || e1 @ E {{ Φ }}.
 Proof.
   intros.
   rewrite -(wp_lift_pure_step E (λ e2' ef', e2 = e2' ∧ ef = ef') _ e1) //=.
diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index 6c08ed1bce7d8334dbaacab23bfdac1a4ff14bd4..28f4f2ac7352672af8f34d624c4656a7c7069536 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -51,6 +51,13 @@ Next Obligation.
 Qed.
 Instance: Params (@wp) 4.
 
+Notation "|| e @ E {{ Φ } }" := (wp E e Φ)
+  (at level 20, e, Φ at level 200,
+   format "||  e  @  E  {{  Φ  } }") : uPred_scope.
+Notation "|| e {{ Φ } }" := (wp ⊤ e Φ)
+  (at level 20, e, Φ at level 200,
+   format "||  e   {{  Φ  } }") : uPred_scope.
+
 Section wp.
 Context {Λ : language} {Σ : iFunctor}.
 Implicit Types P : iProp Λ Σ.
@@ -81,7 +88,7 @@ Proof.
   by intros Φ Φ' ?; apply equiv_dist=>n; apply wp_ne=>v; apply equiv_dist.
 Qed.
 Lemma wp_mask_frame_mono E1 E2 e Φ Ψ :
-  E1 ⊆ E2 → (∀ v, Φ v ⊑ Ψ v) → wp E1 e Φ ⊑ wp E2 e Ψ.
+  E1 ⊆ E2 → (∀ v, Φ v ⊑ Ψ v) → || e @ E1 {{ Φ }} ⊑ || e @ E2 {{ Ψ }}.
 Proof.
   intros HE HΦ n r; revert e r; induction n as [n IH] using lt_wf_ind=> e r.
   destruct 2 as [n' r v HpvsQ|n' r e1 ? Hgo].
@@ -95,19 +102,20 @@ Proof.
   exists r2, r2'; split_and?; [rewrite HE'|eapply IH|]; eauto.
 Qed.
 
-Lemma wp_value_inv E Φ v n r : wp E (of_val v) Φ n r → (|={E}=> Φ v)%I n r.
+Lemma wp_value_inv E Φ v n r :
+  || of_val v @ E {{ Φ }}%I n r → (|={E}=> Φ v)%I n r.
 Proof.
   by inversion 1 as [|??? He]; [|rewrite ?to_of_val in He]; simplify_eq.
 Qed.
 Lemma wp_step_inv E Ef Φ e k n σ r rf :
   to_val e = None → 0 < k < n → E ∩ Ef = ∅ →
-  wp E e Φ n r → wsat (S k) (E ∪ Ef) σ (r ⋅ rf) →
+  || e @ E {{ Φ }}%I n r → wsat (S k) (E ∪ Ef) σ (r ⋅ rf) →
   wp_go (E ∪ Ef) (λ e, wp E e Φ) (λ e, wp ⊤ e (λ _, True%I)) k rf e σ.
 Proof. intros He; destruct 3; [by rewrite ?to_of_val in He|eauto]. Qed.
 
-Lemma wp_value' E Φ v : Φ v ⊑ wp E (of_val v) Φ.
+Lemma wp_value' E Φ v : Φ v ⊑ || of_val v @ E {{ Φ }}.
 Proof. by constructor; apply pvs_intro. Qed.
-Lemma pvs_wp E e Φ : (|={E}=> wp E e Φ) ⊑ wp E e Φ.
+Lemma pvs_wp E e Φ : (|={E}=> || e @ E {{ Φ }}) ⊑ || e @ E {{ Φ }}.
 Proof.
   intros n r ? Hvs.
   destruct (to_val e) as [v|] eqn:He; [apply of_to_val in He; subst|].
@@ -117,7 +125,7 @@ Proof.
   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 Φ : || e @  E {{ λ v, |={E}=> Φ v }} ⊑ || e @ E {{ Φ }}.
 Proof.
   intros n r; revert e r; induction n as [n IH] using lt_wf_ind=> e r Hr HΦ.
   destruct (to_val e) as [v|] eqn:He; [apply of_to_val in He; subst|].
@@ -129,7 +137,8 @@ Proof.
   exists r2, r2'; split_and?; [|apply (IH k)|]; auto.
 Qed.
 Lemma wp_atomic E1 E2 e Φ :
-  E2 ⊆ E1 → atomic e → (|={E1,E2}=> wp E2 e (λ v, |={E2,E1}=> Φ v)) ⊑ wp E1 e Φ.
+  E2 ⊆ E1 → atomic e →
+  (|={E1,E2}=> || e @ E2 {{ λ v, |={E2,E1}=> Φ v }}) ⊑ || e @ E1 {{ Φ }}.
 Proof.
   intros ? He n r ? Hvs; constructor; eauto using atomic_not_val.
   intros rf k Ef σ1 ???.
@@ -146,7 +155,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 : (|| e @ E {{ Φ }} ★ R) ⊑ || e @ E {{ λ v, Φ v ★ R }}.
 Proof.
   intros n r' Hvalid (r&rR&Hr&Hwp&?); revert Hvalid.
   rewrite Hr; clear Hr; revert e r Hwp.
@@ -164,7 +173,7 @@ Proof.
   - apply IH; eauto using uPred_weaken.
 Qed.
 Lemma wp_frame_later_r E e Φ R :
-  to_val e = None → (wp E e Φ ★ ▷ R) ⊑ wp E e (λ v, Φ v ★ R).
+  to_val e = None → (|| e @ E {{ Φ }} ★ ▷ R) ⊑ || e @ E {{ λ v, Φ v ★ R }}.
 Proof.
   intros He n r' Hvalid (r&rR&Hr&Hwp&?); revert Hvalid; rewrite Hr; clear Hr.
   destruct Hwp as [|n r e ? Hgo]; [by rewrite to_of_val in He|].
@@ -178,7 +187,7 @@ Proof.
     eapply uPred_weaken with n rR; eauto.
 Qed.
 Lemma wp_bind `{LanguageCtx Λ K} E e Φ :
-  wp E e (λ v, wp E (K (of_val v)) Φ) ⊑ wp E (K e) Φ.
+  || e @ E {{ λ v, || K (of_val v) @ E {{ Φ }} }} ⊑ || K e @ E {{ Φ }}.
 Proof.
   intros n r; revert e r; induction n as [n IH] using lt_wf_ind=> e r ?.
   destruct 1 as [|n r e ? Hgo]; [by apply pvs_wp|].
@@ -196,39 +205,44 @@ Qed.
 (** * Derived rules *)
 Opaque uPred_holds.
 Import uPred.
-Lemma wp_mono E e Φ Ψ : (∀ v, Φ v ⊑ Ψ v) → wp E e Φ ⊑ wp E e Ψ.
+Lemma wp_mono E e Φ Ψ : (∀ v, Φ v ⊑ Ψ v) → || e @ E {{ Φ }} ⊑ || e @ E {{ Ψ }}.
 Proof. by apply wp_mask_frame_mono. Qed.
 Global Instance wp_mono' E e :
   Proper (pointwise_relation _ (⊑) ==> (⊑)) (@wp Λ Σ E e).
 Proof. by intros Φ Φ' ?; apply wp_mono. Qed.
-Lemma wp_strip_pvs E e P Φ : P ⊑ wp E e Φ → (|={E}=> P) ⊑ wp E e Φ.
+Lemma wp_strip_pvs E e P Φ :
+  P ⊑ || e @ E {{ Φ }} → (|={E}=> P) ⊑ || e @ E {{ Φ }}.
 Proof. move=>->. by rewrite pvs_wp. Qed.
-Lemma wp_value E Φ e v : to_val e = Some v → Φ v ⊑ wp E e Φ.
+Lemma wp_value E Φ e v : to_val e = Some v → Φ v ⊑ || e @ E {{ Φ }}.
 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 Φ.
+Lemma wp_value_pvs E Φ e v :
+  to_val e = Some v → (|={E}=> Φ v) ⊑ || 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 ★ || e @ E {{ Φ }}) ⊑ || e @ E {{ λ v, R ★ Φ v }}.
 Proof. setoid_rewrite (comm _ R); apply wp_frame_r. Qed.
 Lemma wp_frame_later_l E e Φ R :
-  to_val e = None → (▷ R ★ wp E e Φ) ⊑ wp E e (λ v, R ★ Φ v).
+  to_val e = None → (▷ R ★ || e @ E {{ Φ }}) ⊑ || e @ E {{ λ v, R ★ Φ v }}.
 Proof.
   rewrite (comm _ (â–· R)%I); setoid_rewrite (comm _ R).
   apply wp_frame_later_r.
 Qed.
 Lemma wp_always_l E e Φ R `{!AlwaysStable R} :
-  (R ∧ wp E e Φ) ⊑ wp E e (λ v, R ∧ Φ v).
+  (R ∧ || e @ E {{ Φ }}) ⊑ || 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 `{!AlwaysStable R} :
-  (wp E e Φ ∧ R) ⊑ wp E e (λ v, Φ v ∧ R).
+  (|| e @ E {{ Φ }} ∧ R) ⊑ || e @ E {{ λ v, Φ v ∧ R }}.
 Proof. by setoid_rewrite (always_and_sep_r _ _); rewrite wp_frame_r. Qed.
-Lemma wp_impl_l E e Φ Ψ : ((□ ∀ v, Φ v → Ψ v) ∧ wp E e Φ) ⊑ wp E e Ψ.
+Lemma wp_impl_l E e Φ Ψ :
+  ((□ ∀ v, Φ v → Ψ v) ∧ || e @ E {{ Φ }}) ⊑ || e @ E {{ Ψ }}.
 Proof.
   rewrite wp_always_l; apply wp_mono=> // v.
   by rewrite always_elim (forall_elim v) impl_elim_l.
 Qed.
-Lemma wp_impl_r E e Φ Ψ : (wp E e Φ ∧ □ ∀ v, Φ v → Ψ v) ⊑ wp E e Ψ.
+Lemma wp_impl_r E e Φ Ψ :
+  (|| e @ E {{ Φ }} ∧ □ (∀ v, Φ v → Ψ v)) ⊑ || e @ E {{ Ψ }}.
 Proof. by rewrite comm wp_impl_l. Qed.
-Lemma wp_mask_weaken E1 E2 e Φ : E1 ⊆ E2 → wp E1 e Φ ⊑ wp E2 e Φ.
+Lemma wp_mask_weaken E1 E2 e Φ :
+  E1 ⊆ E2 → || e @ E1 {{ Φ }} ⊑ || e @ E2 {{ Φ }}.
 Proof. auto using wp_mask_frame_mono. Qed.
 
 (** * Weakest-pre is a FSA. *)