diff --git a/algebra/cmra.v b/algebra/cmra.v
index 93126eeccad0561ce9a7e4f7f9f894cea1fdd9cf..534341d7e0f1e764c21b5afbac3d774be0df69e8 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -21,7 +21,7 @@ Infix "⩪" := minus (at level 40) : C_scope.
 Class ValidN (A : Type) := validN : nat → A → Prop.
 Instance: Params (@validN) 3.
 Notation "✓{ n } x" := (validN n x)
-  (at level 20, n at level 1, format "✓{ n }  x").
+  (at level 20, n at next level, format "✓{ n }  x").
 
 Class Valid (A : Type) := valid : A → Prop.
 Instance: Params (@valid) 2.
@@ -30,7 +30,7 @@ Instance validN_valid `{ValidN A} : Valid A := λ x, ∀ n, ✓{n} x.
 
 Definition includedN `{Dist A, Op A} (n : nat) (x y : A) := ∃ z, y ≡{n}≡ x ⋅ z.
 Notation "x ≼{ n } y" := (includedN n x y)
-  (at level 70, format "x  ≼{ n }  y") : C_scope.
+  (at level 70, n at next level, format "x  ≼{ n }  y") : C_scope.
 Instance: Params (@includedN) 4.
 Hint Extern 0 (_ ≼{_} _) => reflexivity.
 
@@ -476,7 +476,7 @@ Section discrete.
   Qed.
   Definition discrete_extend_mixin : CMRAExtendMixin A.
   Proof.
-    intros n x y1 y2 ??; exists (y1,y2); split_ands; auto.
+    intros n x y1 y2 ??; exists (y1,y2); split_and?; auto.
     apply (timeless _), dist_le with n; auto with lia.
   Qed.
   Definition discreteRA : cmraT :=
diff --git a/algebra/dra.v b/algebra/dra.v
index f4c126cc84a63d17f2fc9a887c1e5f68c3b88509..a6ef06249b153a1109e69488cf0423f5c6a40de0 100644
--- a/algebra/dra.v
+++ b/algebra/dra.v
@@ -104,13 +104,13 @@ Definition validity_ra : RA (discreteC T).
 Proof.
   split.
   - intros ??? [? Heq]; split; simpl; [|by intros (?&?&?); rewrite Heq].
-    split; intros (?&?&?); split_ands';
+    split; intros (?&?&?); split_and!;
       first [rewrite ?Heq; tauto|rewrite -?Heq; tauto|tauto].
   - by intros ?? [? Heq]; split; [done|]; simpl; intros ?; rewrite Heq.
   - intros ?? [??]; naive_solver.
   - intros x1 x2 [? Hx] y1 y2 [? Hy];
       split; simpl; [|by intros (?&?&?); rewrite Hx // Hy].
-    split; intros (?&?&z&?&?); split_ands'; try tauto.
+    split; intros (?&?&z&?&?); split_and!; try tauto.
     + exists z. by rewrite -Hy // -Hx.
     + exists z. by rewrite Hx ?Hy; tauto.
   - intros [x px ?] [y py ?] [z pz ?]; split; simpl;
@@ -135,7 +135,7 @@ Lemma validity_update (x y : validityRA) :
   (∀ z, ✓ x → ✓ z → validity_car x ⊥ z → ✓ y ∧ validity_car y ⊥ z) → x ~~> y.
 Proof.
   intros Hxy. apply discrete_update.
-  intros z (?&?&?); split_ands'; try eapply Hxy; eauto.
+  intros z (?&?&?); split_and!; try eapply Hxy; eauto.
 Qed.
 
 Lemma to_validity_valid (x : A) :
diff --git a/algebra/iprod.v b/algebra/iprod.v
index 6911be9bd5abe49c9278aa1e1b668edfe2e026fe..8b46f6293b1a41f86412a7f07e2f640108e6479e 100644
--- a/algebra/iprod.v
+++ b/algebra/iprod.v
@@ -156,7 +156,7 @@ Section iprod_cmra.
     intros n f f1 f2 Hf Hf12.
     set (g x := cmra_extend_op n (f x) (f1 x) (f2 x) (Hf x) (Hf12 x)).
     exists ((λ x, (proj1_sig (g x)).1), (λ x, (proj1_sig (g x)).2)).
-    split_ands; intros x; apply (proj2_sig (g x)).
+    split_and?; intros x; apply (proj2_sig (g x)).
   Qed.
   Canonical Structure iprodRA : cmraT :=
     CMRAT iprod_cofe_mixin iprod_cmra_mixin iprod_cmra_extend_mixin.
diff --git a/algebra/option.v b/algebra/option.v
index 3882532bd7108204008187e7566d391175dc21f3..777219d00e2bd3a8133e438367af51be4d91eb06 100644
--- a/algebra/option.v
+++ b/algebra/option.v
@@ -75,7 +75,7 @@ Proof.
   - intros [mz Hmz].
     destruct mx as [x|]; [right|by left].
     destruct my as [y|]; [exists x, y|destruct mz; inversion_clear Hmz].
-    destruct mz as [z|]; inversion_clear Hmz; split_ands; auto;
+    destruct mz as [z|]; inversion_clear Hmz; split_and?; auto;
       cofe_subst; eauto using cmra_includedN_l.
   - intros [->|(x&y&->&->&z&Hz)]; try (by exists my; destruct my; constructor).
     by exists (Some z); constructor.
diff --git a/algebra/sts.v b/algebra/sts.v
index 6868c3187f30287b01a98d1c00a47a12c11f5618..b4244d4393c1dd7e0255595abdb1211dff728a99 100644
--- a/algebra/sts.v
+++ b/algebra/sts.v
@@ -101,7 +101,7 @@ Lemma step_closed s1 s2 T1 T2 S Tf :
   step (s1,T1) (s2,T2) → closed S Tf → s1 ∈ S → T1 ∩ Tf ≡ ∅ →
   s2 ∈ S ∧ T2 ∩ Tf ≡ ∅ ∧ tok s2 ∩ T2 ≡ ∅.
 Proof.
-  inversion_clear 1 as [???? HR Hs1 Hs2]; intros [?? Hstep]??; split_ands; auto.
+  inversion_clear 1 as [???? HR Hs1 Hs2]; intros [?? Hstep]??; split_and?; auto.
   - eapply Hstep with s1, Frame_step with T1 T2; auto with sts.
   - set_solver -Hstep Hs1 Hs2.
 Qed.
@@ -240,7 +240,7 @@ Proof.
     + rewrite (up_closed (up _ _)); auto using closed_up with sts.
     + rewrite (up_closed (up_set _ _));
         eauto using closed_up_set, closed_ne with sts.
-  - intros x y ?? (z&Hy&?&Hxz); exists (unit (x â‹… y)); split_ands.
+  - intros x y ?? (z&Hy&?&Hxz); exists (unit (x â‹… y)); split_and?.
     + destruct Hxz;inversion_clear Hy;constructor;unfold up_set; set_solver.
     + destruct Hxz; inversion_clear Hy; simpl;
         auto using closed_up_set_empty, closed_up_empty with sts.
@@ -326,7 +326,7 @@ Lemma sts_op_auth_frag s S T :
 Proof.
   intros; split; [split|constructor; set_solver]; simpl.
   - intros (?&?&?); by apply closed_disjoint' with S.
-  - intros; split_ands. set_solver+. done. constructor; set_solver.
+  - intros; split_and?. set_solver+. done. constructor; set_solver.
 Qed.
 Lemma sts_op_auth_frag_up s T :
   tok s ∩ T ≡ ∅ → sts_auth s ∅ ⋅ sts_frag_up s T ≡ sts_auth s T.
@@ -381,7 +381,7 @@ when we have RAs back *)
     move:(EQ' Hcl2)=>{EQ'} EQ. inversion_clear EQ as [|? ? ? ? HT HS].
     destruct Hv as [Hv _]. move:(Hv Hcl2)=>{Hv} [/= Hcl1  [Hclf Hdisj]].
     apply Hvf in Hclf. simpl in Hclf. clear Hvf.
-    inversion_clear Hdisj. split; last (exists Tf; split_ands); [done..|].
+    inversion_clear Hdisj. split; last (exists Tf; split_and?); [done..|].
     apply (anti_symm (⊆)).
     + move=>s HS2. apply elem_of_intersection. split; first by apply HS.
       by apply subseteq_up_set.
@@ -392,7 +392,7 @@ when we have RAs back *)
   - intros (Hcl1 & Tf & Htk & Hf & Hs).
     exists (sts_frag (up_set S2 Tf) Tf).
     split; first split; simpl;[|done|].
-    + intros _. split_ands; first done.
+    + intros _. split_and?; first done.
       * apply closed_up_set; last by eapply closed_ne.
         move=>s Hs2. move:(closed_disjoint _ _ Hcl2 _ Hs2).
         set_solver +Htk.
@@ -404,7 +404,7 @@ Lemma sts_frag_included' S1 S2 T :
   closed S2 T → closed S1 T → S2 ≡ S1 ∩ up_set S2 ∅ →
   sts_frag S1 T ≼ sts_frag S2 T.
 Proof.
-  intros. apply sts_frag_included; split_ands; auto.
-  exists ∅; split_ands; done || set_solver+.
+  intros. apply sts_frag_included; split_and?; auto.
+  exists ∅; split_and?; done || set_solver+.
 Qed.
 End stsRA.
diff --git a/algebra/upred.v b/algebra/upred.v
index f83029dd1081ca5036dbf9ec673612a76b89e78e..52c509ca69a496d2a1c3ba2f111dc8f39345409f 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -143,7 +143,7 @@ Next Obligation.
   assert (∃ x2', y ≡{n2}≡ x1 ⋅ x2' ∧ x2 ≼ x2') as (x2'&Hy&?).
   { destruct Hxy as [z Hy]; exists (x2 â‹… z); split; eauto using cmra_included_l.
     apply dist_le with n1; auto. by rewrite (assoc op) -Hx Hy. }
-  clear Hxy; cofe_subst y; exists x1, x2'; split_ands; [done| |].
+  clear Hxy; cofe_subst y; exists x1, x2'; split_and?; [done| |].
   - apply uPred_weaken with n1 x1; eauto using cmra_validN_op_l.
   - apply uPred_weaken with n1 x2; eauto using cmra_validN_op_r.
 Qed.
@@ -273,7 +273,7 @@ Global Instance impl_proper :
 Global Instance sep_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_sep M).
 Proof.
   intros P P' HP Q Q' HQ n' x ??; split; intros (x1&x2&?&?&?); cofe_subst x;
-    exists x1, x2; split_ands; try (apply HP || apply HQ);
+    exists x1, x2; split_and?; try (apply HP || apply HQ);
     eauto using cmra_validN_op_l, cmra_validN_op_r.
 Qed.
 Global Instance sep_proper :
@@ -319,12 +319,13 @@ Proof. intros P1 P2 HP n' x; split; apply HP; eauto using cmra_unit_validN. Qed.
 Global Instance always_proper :
   Proper ((≡) ==> (≡)) (@uPred_always M) := ne_proper _.
 Global Instance ownM_ne n : Proper (dist n ==> dist n) (@uPred_ownM M).
-Proof.
-  by intros a1 a2 Ha n' x; split; intros [a' ?]; exists a'; simpl; first
-    [rewrite -(dist_le _ _ _ _ Ha); last lia
-    |rewrite (dist_le _ _ _ _ Ha); last lia].
-Qed.
-Global Instance ownM_proper : Proper ((≡) ==> (≡)) (@uPred_ownM M) := ne_proper _.
+Proof. move=> a b Ha n' x ? /=. by rewrite (dist_le _ _ _ _ Ha); last lia. Qed.
+Global Instance ownM_proper: Proper ((≡) ==> (≡)) (@uPred_ownM M) := ne_proper _.
+Global Instance valid_ne {A : cmraT} n :
+  Proper (dist n ==> dist n) (@uPred_valid M A).
+Proof. move=> a b Ha n' x ? /=. by rewrite (dist_le _ _ _ _ Ha); last lia. Qed.
+Global Instance valid_proper {A : cmraT} :
+  Proper ((≡) ==> (≡)) (@uPred_valid M A) := ne_proper _.
 Global Instance iff_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_iff M).
 Proof. unfold uPred_iff; solve_proper. Qed.
 Global Instance iff_proper :
@@ -563,17 +564,17 @@ Qed.
 Global Instance sep_assoc : Assoc (≡) (@uPred_sep M).
 Proof.
   intros P Q R n x ?; split.
-  - intros (x1&x2&Hx&?&y1&y2&Hy&?&?); exists (x1 â‹… y1), y2; split_ands; auto.
+  - intros (x1&x2&Hx&?&y1&y2&Hy&?&?); exists (x1 â‹… y1), y2; split_and?; auto.
     + by rewrite -(assoc op) -Hy -Hx.
     + by exists x1, y1.
-  - intros (x1&x2&Hx&(y1&y2&Hy&?&?)&?); exists y1, (y2 â‹… x2); split_ands; auto.
+  - intros (x1&x2&Hx&(y1&y2&Hy&?&?)&?); exists y1, (y2 â‹… x2); split_and?; auto.
     + by rewrite (assoc op) -Hy -Hx.
     + by exists y2, x2.
 Qed.
 Lemma wand_intro_r P Q R : (P ★ Q) ⊑ R → P ⊑ (Q -★ R).
 Proof.
   intros HPQR n x ?? n' x' ???; apply HPQR; auto.
-  exists x, x'; split_ands; auto.
+  exists x, x'; split_and?; auto.
   eapply uPred_weaken with n x; eauto using cmra_validN_op_l.
 Qed.
 Lemma wand_elim_l P Q : ((P -★ Q) ★ P) ⊑ Q.
diff --git a/barrier/barrier.v b/barrier/barrier.v
index 5439e69cf9611751246c37a2436f497d91b91758..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.
 
@@ -260,14 +260,14 @@ Section spec.
   Lemma barrier_spec (heapN N : namespace) :
     heapN ⊥ N →
     ∃ (recv send : loc -> iProp -n> iProp),
-      (∀ P, heap_ctx heapN ⊑ ({{ True }} newchan '() @ ⊤ {{ λ v, ∃ l, 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 Q, {{ recv l (P ★ Q) }} Skip @ ⊤ {{ λ _, recv l P ★ recv l Q }}) ∧
+      (∀ P, heap_ctx heapN ⊑ ({{ True }} newchan '() {{ λ v, ∃ l, 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 Q, {{ recv l (P ★ Q) }} Skip {{ λ _, recv l P ★ recv l Q }}) ∧
       (∀ l P Q, (P -★ Q) ⊑ (recv l P -★ recv l Q)).
   Proof.
     intros HN. exists (λ l, CofeMor (recv N heapN l)). exists (λ l, CofeMor (send N heapN l)).
-    split_ands; cbn.
+    split_and?; cbn.
     - intros. apply: always_intro. apply impl_intro_l. rewrite -newchan_spec.
       rewrite comm always_and_sep_r. apply sep_mono_r. apply forall_intro=>l.
       apply wand_intro_l. rewrite right_id -(exist_intro l) const_equiv // left_id.
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 e52dadfd4d900cf043bf87eb83eaad241a990cc8..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 σ ⊑ pvs E 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,10 +100,10 @@ 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 (pvs E E (auth_own heap_name ∅ ★ P))%I.
+    transitivity (|={E}=> auth_own heap_name ∅ ★ P)%I.
     { by rewrite -pvs_frame_r -(auth_empty _ E) left_id. }
     apply wp_strip_pvs, (auth_fsa heap_inv (wp_fsa (Alloc e)))
       with N heap_name ∅; simpl; eauto with 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 afc88d836827f1eeb8e178c48e66d590c72ea537..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.
@@ -86,7 +87,7 @@ Section ClosedProofs.
   Instance: authG heap_lang Σ heapRA.
   Proof. split; try apply _. by exists 1%nat. Qed.
 
-  Lemma heap_e_hoare σ : {{ ownP σ : iProp }} heap_e @ ⊤ {{ λ v, v = '2 }}.
+  Lemma heap_e_hoare σ : {{ ownP σ : iProp }} heap_e {{ λ v, v = '2 }}.
   Proof.
     apply ht_alt. rewrite (heap_alloc ⊤ nroot); last by rewrite nclose_nroot.
     apply wp_strip_pvs, exist_elim=> ?. rewrite and_elim_l.
diff --git a/prelude/fin_maps.v b/prelude/fin_maps.v
index 1306a3218b3635e5ac6cb152eb974f612c971f6a..0f3ec1cbbcec2aae19542fad18021a07cd765dbd 100644
--- a/prelude/fin_maps.v
+++ b/prelude/fin_maps.v
@@ -476,7 +476,7 @@ Lemma insert_subset_inv {A} (m1 m2 : M A) i x :
   m1 !! i = None → <[i:=x]> m1 ⊂ m2 →
   ∃ m2', m2 = <[i:=x]>m2' ∧ m1 ⊂ m2' ∧ m2' !! i = None.
 Proof.
-  intros Hi Hm1m2. exists (delete i m2). split_ands.
+  intros Hi Hm1m2. exists (delete i m2). split_and?.
   - rewrite insert_delete. done. eapply lookup_weaken, strict_include; eauto.
     by rewrite lookup_insert.
   - eauto using insert_delete_subset.
diff --git a/prelude/finite.v b/prelude/finite.v
index 20f53f53df6b5c142ff09cba1d5f0758dfa4a34c..4075de942d5cbf4c2f40408410b77c6c43cc2df3 100644
--- a/prelude/finite.v
+++ b/prelude/finite.v
@@ -220,7 +220,7 @@ Proof. done. Qed.
 Program Instance sum_finite `{Finite A, Finite B} : Finite (A + B)%type :=
   {| enum := (inl <$> enum A) ++ (inr <$> enum B) |}.
 Next Obligation.
-  intros. apply NoDup_app; split_ands.
+  intros. apply NoDup_app; split_and?.
   - apply (NoDup_fmap_2 _). by apply NoDup_enum.
   - intro. rewrite !elem_of_list_fmap. intros (?&?&?) (?&?&?); congruence.
   - apply (NoDup_fmap_2 _). by apply NoDup_enum.
@@ -237,7 +237,7 @@ Program Instance prod_finite `{Finite A, Finite B} : Finite (A * B)%type :=
 Next Obligation.
   intros ??????. induction (NoDup_enum A) as [|x xs Hx Hxs IH]; simpl.
   { constructor. }
-  apply NoDup_app; split_ands.
+  apply NoDup_app; split_and?.
   - by apply (NoDup_fmap_2 _), NoDup_enum.
   - intros [? y]. rewrite elem_of_list_fmap. intros (?&?&?); simplify_eq.
     clear IH. induction Hxs as [|x' xs ?? IH]; simpl.
@@ -271,7 +271,7 @@ Next Obligation.
   intros ????. induction n as [|n IH]; simpl; [apply NoDup_singleton |].
   revert IH. generalize (list_enum (enum A) n). intros l Hl.
   induction (NoDup_enum A) as [|x xs Hx Hxs IH]; simpl; auto; [constructor |].
-  apply NoDup_app; split_ands.
+  apply NoDup_app; split_and?.
   - by apply (NoDup_fmap_2 _).
   - intros [k1 Hk1]. clear Hxs IH. rewrite elem_of_list_fmap.
     intros ([k2 Hk2]&?&?) Hxk2; simplify_eq/=. destruct Hx. revert Hxk2.
diff --git a/prelude/hashset.v b/prelude/hashset.v
index f7142566660b29fc97eba1854088e800ae65b837..eaa109bd455d8a6b0498708e9b05e04bbf035f69 100644
--- a/prelude/hashset.v
+++ b/prelude/hashset.v
@@ -85,7 +85,7 @@ Proof.
       rewrite elem_of_list_intersection in Hx; naive_solver. }
     intros [(l&?&?) (k&?&?)]. assert (x ∈ list_intersection l k)
       by (by rewrite elem_of_list_intersection).
-    exists (list_intersection l k); split; [exists l, k|]; split_ands; auto.
+    exists (list_intersection l k); split; [exists l, k|]; split_and?; auto.
     by rewrite option_guard_True by eauto using elem_of_not_nil.
   - unfold elem_of, hashset_elem_of, intersection, hashset_intersection.
     intros [m1 ?] [m2 ?] x; simpl.
@@ -95,7 +95,7 @@ Proof.
     intros [(l&?&?) Hm2]; destruct (m2 !! hash x) as [k|] eqn:?; eauto.
     destruct (decide (x ∈ k)); [destruct Hm2; eauto|].
     assert (x ∈ list_difference l k) by (by rewrite elem_of_list_difference).
-    exists (list_difference l k); split; [right; exists l,k|]; split_ands; auto.
+    exists (list_difference l k); split; [right; exists l,k|]; split_and?; auto.
     by rewrite option_guard_True by eauto using elem_of_not_nil.
   - unfold elem_of at 2, hashset_elem_of, elements, hashset_elems.
     intros [m Hm] x; simpl. setoid_rewrite elem_of_list_bind. split.
@@ -107,7 +107,7 @@ Proof.
     rewrite map_Forall_to_list in Hm. generalize (NoDup_fst_map_to_list m).
     induction Hm as [|[n l] m' [??]];
       csimpl; inversion_clear 1 as [|?? Hn]; [constructor|].
-    apply NoDup_app; split_ands; eauto.
+    apply NoDup_app; split_and?; eauto.
     setoid_rewrite elem_of_list_bind; intros x ? ([n' l']&?&?); simpl in *.
     assert (hash x = n ∧ hash x = n') as [??]; subst.
     { split; [eapply (Forall_forall (λ x, hash x = n) l); eauto|].
diff --git a/prelude/pretty.v b/prelude/pretty.v
index 180a87b2be1aac2e23bd1ba43c100feac638f79f..e676fe82f7712c9e163e1393502566257d1c478a 100644
--- a/prelude/pretty.v
+++ b/prelude/pretty.v
@@ -57,7 +57,7 @@ Proof.
   { intros -> Hlen; edestruct help; rewrite Hlen; simpl; lia. }
   { intros <- Hlen; edestruct help; rewrite <-Hlen; simpl; lia. }
   intros Hs Hlen; apply IH in Hs; destruct Hs;
-    simplify_eq/=; split_ands'; auto using N.div_lt_upper_bound with lia.
+    simplify_eq/=; split_and?; auto using N.div_lt_upper_bound with lia.
   rewrite (N.div_mod x 10), (N.div_mod y 10) by done.
   auto using N.mod_lt with f_equal.
 Qed.
diff --git a/prelude/tactics.v b/prelude/tactics.v
index f2df02d5dbd8d277631b68fbc21396b929713c4b..120bf0fec279b65d81f9707482d47f3e2bb405db 100644
--- a/prelude/tactics.v
+++ b/prelude/tactics.v
@@ -54,11 +54,20 @@ Ltac done :=
 Tactic Notation "by" tactic(tac) :=
   tac; done.
 
-(** Whereas the [split] tactic splits any inductive with one constructor, the
-tactic [split_and] only splits a conjunction. *)
-Ltac split_and := match goal with |- _ ∧ _ => split end.
-Ltac split_ands := repeat split_and.
-Ltac split_ands' := repeat (hnf; split_and).
+(** Tactics for splitting conjunctions:
+
+- [split_and] : split the goal if is syntactically of the shape [_ ∧ _]
+- [split_ands?] : split the goal repeatedly (perhaps zero times) while it is
+  of the shape [_ ∧ _].
+- [split_ands!] : works similarly, but at least one split should succeed. In
+  order to do so, it will head normalize the goal first to possibly expose a
+  conjunction.
+
+Note that [split_and] differs from [split] by only splitting conjunctions. The
+[split] tactic splits any inductive with one constructor. *)
+Tactic Notation "split_and" := match goal with |- _ ∧ _ => split end.
+Tactic Notation "split_and" "?" := repeat split_and.
+Tactic Notation "split_and" "!" := hnf; split_and; split_and?.
 
 (** The tactic [case_match] destructs an arbitrary match in the conclusion or
 assumptions, and generates a corresponding equality. This tactic is best used
diff --git a/prelude/zmap.v b/prelude/zmap.v
index aa96fabb48fcec68490de8fe5198e9eb532fa03e..c80d7f71051ddf6a51c1974c11e017010973d439 100644
--- a/prelude/zmap.v
+++ b/prelude/zmap.v
@@ -64,7 +64,7 @@ Proof.
   - intros ? [o t t']; unfold map_to_list; simpl.
     assert (NoDup ((prod_map Z.pos id <$> map_to_list t) ++
       prod_map Z.neg id <$> map_to_list t')).
-    { apply NoDup_app; split_ands.
+    { apply NoDup_app; split_and?.
       - apply (NoDup_fmap_2 _), NoDup_map_to_list.
       - intro. rewrite !elem_of_list_fmap. naive_solver.
       - apply (NoDup_fmap_2 _), NoDup_map_to_list. }
diff --git a/program_logic/adequacy.v b/program_logic/adequacy.v
index d7f0609df65ca4f706f86087306a37089b8ef9ee..6ddf73e2fc44a1dac72c112ef975e219bb13476f 100644
--- a/program_logic/adequacy.v
+++ b/program_logic/adequacy.v
@@ -53,7 +53,7 @@ Proof.
     by rewrite -Permutation_middle /= big_op_app.
 Qed.
 Lemma ht_adequacy_steps P Φ k n e1 t2 σ1 σ2 r1 :
-  {{ P }} e1 @ ⊤ {{ Φ }} →
+  {{ P }} e1 {{ Φ }} →
   nsteps step k ([e1],σ1) (t2,σ2) →
   1 < n → wsat (k + n) ⊤ σ1 r1 →
   P (k + n) r1 →
@@ -66,15 +66,15 @@ Proof.
   eapply uPred.const_intro; eauto.
 Qed.
 Lemma ht_adequacy_own Φ e1 t2 σ1 m σ2 :
-  ✓m →
-  {{ ownP σ1 ★ ownG m }} e1 @ ⊤ {{ Φ }} →
+  ✓ m →
+  {{ ownP σ1 ★ ownG m }} e1 {{ Φ }} →
   rtc step ([e1],σ1) (t2,σ2) →
   ∃ rs2 Φs', wptp 2 t2 (Φ :: Φs') rs2 ∧ wsat 2 ⊤ σ2 (big_op rs2).
 Proof.
   intros Hv ? [k ?]%rtc_nsteps.
   eapply ht_adequacy_steps with (r1 := (Res ∅ (Excl σ1) (Some m))); eauto; [|].
   { by rewrite Nat.add_comm; apply wsat_init, cmra_valid_validN. }
-  exists (Res ∅ (Excl σ1) ∅), (Res ∅ ∅ (Some m)); split_ands.
+  exists (Res ∅ (Excl σ1) ∅), (Res ∅ ∅ (Some m)); split_and?.
   - by rewrite Res_op ?left_id ?right_id.
   - by rewrite /uPred_holds /=.
   - by apply ownG_spec.
diff --git a/program_logic/auth.v b/program_logic/auth.v
index 0ce603866f59e4bd4f79fb05601a7bc99dce6d20..65e54aeca55e587939c1775b9f74bbae232fa902 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -43,7 +43,7 @@ Section auth.
 
   Lemma auth_alloc E N a :
     ✓ a → nclose N ⊆ E →
-    ▷ φ a ⊑ pvs E E (∃ γ, auth_ctx γ N φ ∧ auth_own γ a).
+    ▷ φ a ⊑ (|={E}=> ∃ γ, auth_ctx γ N φ ∧ auth_own γ a).
   Proof.
     intros Ha HN. eapply sep_elim_True_r.
     { by eapply (own_alloc (Auth (Excl a) a) N). }
@@ -58,12 +58,12 @@ Section auth.
     by rewrite always_and_sep_l.
   Qed.
 
-  Lemma auth_empty γ E : True ⊑ pvs E E (auth_own γ ∅).
+  Lemma auth_empty γ E : True ⊑ (|={E}=> auth_own γ ∅).
   Proof. by rewrite /auth_own -own_update_empty. Qed.
 
   Lemma auth_opened E γ a :
     (▷ auth_inv γ φ ★ auth_own γ a)
-    ⊑ pvs E E (∃ a', ■ ✓ (a ⋅ a') ★ ▷ φ (a ⋅ a') ★ own γ (● (a ⋅ a') ⋅ ◯ a)).
+    ⊑ (|={E}=> ∃ a', ■ ✓ (a ⋅ a') ★ ▷ φ (a ⋅ a') ★ own γ (● (a ⋅ a') ⋅ ◯ a)).
   Proof.
     rewrite /auth_inv. rewrite later_exist sep_exist_r. apply exist_elim=>b.
     rewrite later_sep [(▷(_ ∧ _))%I]pvs_timeless !pvs_frame_r. apply pvs_mono.
@@ -83,7 +83,7 @@ Section auth.
   Lemma auth_closing `{!LocalUpdate Lv L} E γ a a' :
     Lv a → ✓ (L a ⋅ a') →
     (▷ φ (L a ⋅ a') ★ own γ (● (a ⋅ a') ⋅ ◯ a))
-    ⊑ pvs E E (▷ auth_inv γ φ ★ auth_own γ (L a)).
+    ⊑ (|={E}=> ▷ auth_inv γ φ ★ auth_own γ (L a)).
   Proof.
     intros HL Hv. rewrite /auth_inv /auth_own -(exist_intro (L a â‹… a')).
     rewrite later_sep [(_ ★ ▷φ _)%I]comm -assoc.
diff --git a/program_logic/ghost_ownership.v b/program_logic/ghost_ownership.v
index 83b0a23823a32c849ce39182f6fb96b18e18af46..e17065f75a89b9f5e90da522a39899070098aee9 100644
--- a/program_logic/ghost_ownership.v
+++ b/program_logic/ghost_ownership.v
@@ -91,7 +91,7 @@ Proof. by rewrite /AlwaysStable always_own_unit. Qed.
 (* TODO: This also holds if we just have ✓ a at the current step-idx, as Iris
    assertion. However, the map_updateP_alloc does not suffice to show this. *)
 Lemma own_alloc_strong a E (G : gset gname) :
-  ✓ a → True ⊑ pvs E E (∃ γ, ■(γ ∉ G) ∧ own γ a).
+  ✓ a → True ⊑ (|={E}=> ∃ γ, ■(γ ∉ G) ∧ own γ a).
 Proof.
   intros Ha.
   rewrite -(pvs_mono _ _ (∃ m, ■ (∃ γ, γ ∉ G ∧ m = to_globalF γ a) ∧ ownG m)%I).
@@ -101,14 +101,14 @@ Proof.
   - apply exist_elim=>m; apply const_elim_l=>-[γ [Hfresh ->]].
     by rewrite -(exist_intro γ) const_equiv.
 Qed.
-Lemma own_alloc a E : ✓ a → True ⊑ pvs E E (∃ γ, own γ a).
+Lemma own_alloc a E : ✓ a → True ⊑ (|={E}=> ∃ γ, own γ a).
 Proof.
   intros Ha. rewrite (own_alloc_strong a E ∅) //; []. apply pvs_mono.
   apply exist_mono=>?. eauto with I.
 Qed.
 
 Lemma own_updateP P γ a E :
-  a ~~>: P → own γ a ⊑ pvs E E (∃ a', ■ P a' ∧ own γ a').
+  a ~~>: P → own γ a ⊑ (|={E}=> ∃ a', ■ P a' ∧ own γ a').
 Proof.
   intros Ha.
   rewrite -(pvs_mono _ _ (∃ m, ■ (∃ a', m = to_globalF γ a' ∧ P a') ∧ ownG m)%I).
@@ -120,7 +120,7 @@ Proof.
 Qed.
 
 Lemma own_updateP_empty `{Empty A, !CMRAIdentity A} P γ E :
-  ∅ ~~>: P → True ⊑ pvs E E (∃ a, ■ P a ∧ own γ a).
+  ∅ ~~>: P → True ⊑ (|={E}=> ∃ a, ■ P a ∧ own γ a).
 Proof.
   intros Hemp.
   rewrite -(pvs_mono _ _ (∃ m, ■ (∃ a', m = to_globalF γ a' ∧ P a') ∧ ownG m)%I).
@@ -131,14 +131,14 @@ Proof.
     rewrite -(exist_intro a'). by apply and_intro; [apply const_intro|].
 Qed.
 
-Lemma own_update γ a a' E : a ~~> a' → own γ a ⊑ pvs E E (own γ a').
+Lemma own_update γ a a' E : a ~~> a' → own γ a ⊑ (|={E}=> own γ a').
 Proof.
   intros; rewrite (own_updateP (a' =)); last by apply cmra_update_updateP.
   by apply pvs_mono, exist_elim=> a''; apply const_elim_l=> ->.
 Qed.
 
 Lemma own_update_empty `{Empty A, !CMRAIdentity A} γ E :
-  True ⊑ pvs E E (own γ ∅).
+  True ⊑ (|={E}=> own γ ∅).
 Proof.
   rewrite (own_updateP_empty (∅ =)); last by apply cmra_updateP_id.
   apply pvs_mono, exist_elim=>a. by apply const_elim_l=>->.
diff --git a/program_logic/hoare.v b/program_logic/hoare.v
index 8924ef906b70a6b3888a654d52cad13620ced70a..643f92e9c618e49def2e2a8922e9a65f1f51c2b5 100644
--- a/program_logic/hoare.v
+++ b/program_logic/hoare.v
@@ -1,13 +1,22 @@
 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 Φ)
-  (at level 74, format "{{  P  } }  e  @  E  {{  Φ  } }") : uPred_scope.
+  (at level 20, P, e, Φ at level 200,
+   format "{{  P  } }  e  @  E  {{  Φ  } }") : uPred_scope.
+Notation "{{ P } } e {{ Φ } }" := (ht ⊤ P e Φ)
+  (at level 20, P, e, Φ at level 200,
+   format "{{  P  } }  e  {{  Φ  } }") : uPred_scope.
 Notation "{{ P } } e @ E {{ Φ } }" := (True ⊑ ht E P e Φ)
-  (at level 74, format "{{  P  } }  e  @  E  {{  Φ  } }") : C_scope.
+  (at level 20, P, e, Φ at level 200,
+   format "{{  P  } }  e  @  E  {{  Φ  } }") : C_scope.
+Notation "{{ P } } e {{ Φ } }" := (True ⊑ ht ⊤ P e Φ)
+  (at level 20, P, e, Φ at level 200,
+   format "{{  P  } }  e  {{  Φ  } }") : C_scope.
 
 Section hoare.
 Context {Λ : language} {Σ : iFunctor}.
@@ -29,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/hoare_lifting.v b/program_logic/hoare_lifting.v
index 08245964cc16c7032d58955736d32e39b658c244..cda1417822f8691af3df00fb0d59526dc2faa6c5 100644
--- a/program_logic/hoare_lifting.v
+++ b/program_logic/hoare_lifting.v
@@ -4,10 +4,12 @@ Import uPred.
 
 Local Notation "{{ P } } ef ?@ E {{ Φ } }" :=
   (default True%I ef (λ e, ht E P e Φ))
-  (at level 74, format "{{  P  } }  ef  ?@  E  {{  Φ  } }") : uPred_scope.
+  (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 74, format "{{  P  } }  ef  ?@  E  {{  Φ  } }") : C_scope.
+  (at level 20, P, ef, Φ at level 200,
+   format "{{  P  } }  ef  ?@  E  {{  Φ  } }") : C_scope.
 
 Section lifting.
 Context {Λ : language} {Σ : iFunctor}.
diff --git a/program_logic/invariants.v b/program_logic/invariants.v
index a8b4269559d8af55a30a1ce40fc6406ce2825470..b9dcdea18836e8fb5b42fd35588befeb1ebd4391 100644
--- a/program_logic/invariants.v
+++ b/program_logic/invariants.v
@@ -58,14 +58,14 @@ Lemma pvs_open_close E N P Q R :
   nclose N ⊆ E →
   R ⊑ inv N P →
   R ⊑ (▷ P -★ pvs (E ∖ nclose N) (E ∖ nclose N) (▷ P ★ Q)) →
-  R ⊑ pvs E E Q.
+  R ⊑ (|={E}=> Q).
 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 79e6b0b9bfa21c3552bbf287b426495e4e4a49eb..77cd393d0259e98ada8f51bfeec4be4fc6e0648d 100644
--- a/program_logic/lifting.v
+++ b/program_logic/lifting.v
@@ -23,9 +23,9 @@ Lemma wp_lift_step E1 E2
   E1 ⊆ E2 → to_val e1 = None →
   reducible e1 σ1 →
   (∀ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → φ e2 σ2 ef) →
-  pvs E2 E1 (ownP σ1 ★ ▷ ∀ e2 σ2 ef,
-    (■ φ e2 σ2 ef ∧ ownP σ2) -★ pvs E1 E2 (wp E2 e2 Φ ★ wp_fork ef))
-  ⊑ wp E2 e1 Φ.
+  (|={E2,E1}=> ownP σ1 ★ ▷ ∀ e2 σ2 ef,
+    (■ φ 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')
@@ -38,20 +38,20 @@ Proof.
     as (r'&(r1'&r2'&?&?&?)&?); auto; cofe_subst r'.
   { split. destruct k; try eapply Hstep; eauto. apply ownP_spec; auto. }
   { rewrite (comm _ r2) -assoc; eauto using wsat_le. }
-  by exists r1', r2'; split_ands; [| |by intros ? ->].
+  by exists r1', r2'; split_and?; [| |by intros ? ->].
 Qed.
 
 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.
   intros e2 σ2 ef ?; destruct (Hstep σ1 e2 σ2 ef); auto; subst.
   destruct (Hwp e2 ef k r) as (r1&r2&Hr&?&?); auto.
-  exists r1,r2; split_ands; [rewrite -Hr| |by intros ? ->]; eauto using wsat_le.
+  exists r1,r2; split_and?; [rewrite -Hr| |by intros ? ->]; eauto using wsat_le.
 Qed.
 
 (** Derived lifting lemmas. *)
@@ -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/namespaces.v b/program_logic/namespaces.v
index 77cac1a12ff9f89d98c1331e7e1ce97ca769ead1..78d7cdf4054119b716dfe5f3da8158925ef7a874 100644
--- a/program_logic/namespaces.v
+++ b/program_logic/namespaces.v
@@ -39,7 +39,7 @@ Section ndisjoint.
   Lemma ndot_preserve_disjoint_l N1 N2 x : N1 ⊥ N2 → ndot N1 x ⊥ N2.
   Proof.
     intros (N1' & N2' & Hpr1 & Hpr2 & Hl & Hne). exists N1', N2'.
-    split_ands; try done; []. by apply suffix_of_cons_r.
+    split_and?; try done; []. by apply suffix_of_cons_r.
   Qed.
 
   Lemma ndot_preserve_disjoint_r N1 N2 x : N1 ⊥ N2 → N1 ⊥ ndot N2 x .
diff --git a/program_logic/ownership.v b/program_logic/ownership.v
index 7a971a81719343bdbff083496beb02bf5949ca59..2cbb11caef8aceb0b98da3358866c469c8920777 100644
--- a/program_logic/ownership.v
+++ b/program_logic/ownership.v
@@ -79,7 +79,7 @@ Proof.
   - intros [(P'&Hi&HP) _]; rewrite Hi.
     by apply Some_dist, symmetry, agree_valid_includedN,
       (cmra_included_includedN _ P'),HP; apply map_lookup_validN with (wld r) i.
-  - intros ?; split_ands; try apply cmra_empty_leastN; eauto.
+  - intros ?; split_and?; try apply cmra_empty_leastN; eauto.
 Qed.
 Lemma ownP_spec r n σ : ✓{n} r → (ownP σ) n r ↔ pst r ≡{n}≡ Excl σ.
 Proof.
diff --git a/program_logic/pviewshifts.v b/program_logic/pviewshifts.v
index 6619abfb1e8b67d00cbca4536434594f049b1058..189e50eb83f0552809b289743ad074481513a01b 100644
--- a/program_logic/pviewshifts.v
+++ b/program_logic/pviewshifts.v
@@ -27,6 +27,13 @@ Qed.
 Arguments pvs {_ _} _ _ _%I : simpl never.
 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,
+   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,
+   format "|={ E }=>  Q") : uPred_scope.
+
 Section pvs.
 Context {Λ : language} {Σ : iFunctor}.
 Implicit Types P Q : iProp Λ Σ.
@@ -37,49 +44,49 @@ Global Instance pvs_ne E1 E2 n : Proper (dist n ==> dist n) (@pvs Λ Σ E1 E2).
 Proof.
   intros P Q HPQ r1 n' ??; simpl; split; intros HP rf k Ef σ ???;
     destruct (HP rf k Ef σ) as (r2&?&?); auto;
-    exists r2; split_ands; auto; apply HPQ; eauto.
+    exists r2; split_and?; auto; apply HPQ; eauto.
 Qed.
 Global Instance pvs_proper E1 E2 : Proper ((≡) ==> (≡)) (@pvs Λ Σ E1 E2).
 Proof. apply ne_proper, _. Qed.
 
-Lemma pvs_intro E P : P ⊑ pvs E E P.
+Lemma pvs_intro E P : P ⊑ |={E}=> P.
 Proof.
   intros n r ? HP rf k Ef σ ???; exists r; split; last done.
   apply uPred_weaken with n r; eauto.
 Qed.
-Lemma pvs_mono E1 E2 P Q : P ⊑ Q → pvs E1 E2 P ⊑ pvs E1 E2 Q.
+Lemma pvs_mono E1 E2 P Q : P ⊑ Q → (|={E1,E2}=> P) ⊑ (|={E1,E2}=> Q).
 Proof.
   intros HPQ n r ? HP rf k Ef σ ???.
   destruct (HP rf k Ef σ) as (r2&?&?); eauto; exists r2; eauto.
 Qed.
-Lemma pvs_timeless E P : TimelessP P → (▷ P) ⊑ pvs E E P.
+Lemma pvs_timeless E P : TimelessP P → (▷ P) ⊑ (|={E}=> P).
 Proof.
   rewrite uPred.timelessP_spec=> HP [|n] r ? HP' rf k Ef σ ???; first lia.
   exists r; split; last done.
   apply HP, uPred_weaken with n r; eauto using cmra_validN_le.
 Qed.
 Lemma pvs_trans E1 E2 E3 P :
-  E2 ⊆ E1 ∪ E3 → pvs E1 E2 (pvs E2 E3 P) ⊑ pvs E1 E3 P.
+  E2 ⊆ E1 ∪ E3 → (|={E1,E2}=> |={E2,E3}=> P) ⊑ (|={E1,E3}=> P).
 Proof.
   intros ? n r1 ? HP1 rf k Ef σ ???.
   destruct (HP1 rf k Ef σ) as (r2&HP2&?); auto.
 Qed.
 Lemma pvs_mask_frame E1 E2 Ef P :
-  Ef ∩ (E1 ∪ E2) = ∅ → pvs E1 E2 P ⊑ pvs (E1 ∪ Ef) (E2 ∪ Ef) P.
+  Ef ∩ (E1 ∪ E2) = ∅ → (|={E1,E2}=> P) ⊑ (|={E1 ∪ Ef,E2 ∪ Ef}=> P).
 Proof.
   intros ? n r ? HP rf k Ef' σ ???.
   destruct (HP rf k (Ef∪Ef') σ) as (r'&?&?); rewrite ?(assoc_L _); eauto.
   by exists r'; rewrite -(assoc_L _).
 Qed.
-Lemma pvs_frame_r E1 E2 P Q : (pvs E1 E2 P ★ Q) ⊑ pvs E1 E2 (P ★ Q).
+Lemma pvs_frame_r E1 E2 P Q : ((|={E1,E2}=> P) ★ Q) ⊑ (|={E1,E2}=> P ★ Q).
 Proof.
   intros n r ? (r1&r2&Hr&HP&?) rf k Ef σ ???.
   destruct (HP (r2 ⋅ rf) k Ef σ) as (r'&?&?); eauto.
   { by rewrite assoc -(dist_le _ _ _ _ Hr); last lia. }
   exists (r' â‹… r2); split; last by rewrite -assoc.
-  exists r', r2; split_ands; auto; apply uPred_weaken with n r2; auto.
+  exists r', r2; split_and?; auto; apply uPred_weaken with n r2; auto.
 Qed.
-Lemma pvs_openI i P : ownI i P ⊑ pvs {[ i ]} ∅ (▷ P).
+Lemma pvs_openI i P : ownI i P ⊑ (|={{[i]},∅}=> ▷ P).
 Proof.
   intros [|n] r ? Hinv rf [|k] Ef σ ???; try lia.
   apply ownI_spec in Hinv; last auto.
@@ -88,7 +95,7 @@ Proof.
   exists (rP â‹… r); split; last by rewrite (left_id_L _ _) -assoc.
   eapply uPred_weaken with (S k) rP; eauto using cmra_included_l.
 Qed.
-Lemma pvs_closeI i P : (ownI i P ∧ ▷ P) ⊑ pvs ∅ {[ i ]} True.
+Lemma pvs_closeI i P : (ownI i P ∧ ▷ P) ⊑ (|={∅,{[i]}}=> True).
 Proof.
   intros [|n] r ? [? HP] rf [|k] Ef σ ? HE ?; try lia; exists ∅; split; [done|].
   rewrite left_id; apply wsat_close with P r.
@@ -98,7 +105,7 @@ Proof.
   - apply uPred_weaken with n r; auto.
 Qed.
 Lemma pvs_ownG_updateP E m (P : iGst Λ Σ → Prop) :
-  m ~~>: P → ownG m ⊑ pvs E E (∃ m', ■ P m' ∧ ownG m').
+  m ~~>: P → ownG m ⊑ (|={E}=> ∃ m', ■ P m' ∧ ownG m').
 Proof.
   intros Hup%option_updateP' [|n] r ? Hinv%ownG_spec rf [|k] Ef σ ???; try lia.
   destruct (wsat_update_gst k (E ∪ Ef) σ r rf (Some m) P) as (m'&?&?); eauto.
@@ -107,7 +114,7 @@ Proof.
 Qed.
 Lemma pvs_ownG_updateP_empty `{Empty (iGst Λ Σ), !CMRAIdentity (iGst Λ Σ)}
     E (P : iGst Λ Σ → Prop) :
-  ∅ ~~>: P → True ⊑ pvs E E (∃ m', ■ P m' ∧ ownG m').
+  ∅ ~~>: P → True ⊑ (|={E}=> ∃ m', ■ P m' ∧ ownG m').
 Proof.
   intros Hup [|n] r ? _ rf [|k] Ef σ ???; try lia.
   destruct (wsat_update_gst k (E ∪ Ef) σ r rf ∅ P) as (m'&?&?); eauto.
@@ -116,7 +123,7 @@ Proof.
       auto using option_update_None. }
   by exists (update_gst m' r); split; [exists m'; split; [|apply ownG_spec]|].
 Qed.
-Lemma pvs_allocI E P : ¬set_finite E → ▷ P ⊑ pvs E E (∃ i, ■ (i ∈ E) ∧ ownI i P).
+Lemma pvs_allocI E P : ¬set_finite E → ▷ P ⊑ (|={E}=> ∃ i, ■ (i ∈ E) ∧ ownI i P).
 Proof.
   intros ? [|n] r ? HP rf [|k] Ef σ ???; try lia.
   destruct (wsat_alloc k E Ef σ rf P r) as (i&?&?&?); auto.
@@ -130,40 +137,41 @@ Opaque uPred_holds.
 Import uPred.
 Global Instance pvs_mono' E1 E2 : Proper ((⊑) ==> (⊑)) (@pvs Λ Σ E1 E2).
 Proof. intros P Q; apply pvs_mono. Qed.
-Lemma pvs_trans' E P : pvs E E (pvs E E P) ⊑ pvs E E P.
+Lemma pvs_trans' E P : (|={E}=> |={E}=> P) ⊑ (|={E}=> P).
 Proof. apply pvs_trans; set_solver. Qed.
-Lemma pvs_strip_pvs E P Q : P ⊑ pvs E E Q → pvs E E P ⊑ pvs E E Q.
+Lemma pvs_strip_pvs E P Q : P ⊑ (|={E}=> Q) → (|={E}=> P) ⊑ (|={E}=> Q).
 Proof. move=>->. by rewrite pvs_trans'. Qed.
-Lemma pvs_frame_l E1 E2 P Q : (P ★ pvs E1 E2 Q) ⊑ pvs E1 E2 (P ★ Q).
+Lemma pvs_frame_l E1 E2 P Q : (P ★ |={E1,E2}=> Q) ⊑ (|={E1,E2}=> P ★ Q).
 Proof. rewrite !(comm _ P); apply pvs_frame_r. Qed.
 Lemma pvs_always_l E1 E2 P Q `{!AlwaysStable P} :
-  (P ∧ pvs E1 E2 Q) ⊑ pvs E1 E2 (P ∧ Q).
+  (P ∧ |={E1,E2}=> Q) ⊑ (|={E1,E2}=> P ∧ Q).
 Proof. by rewrite !always_and_sep_l pvs_frame_l. Qed.
 Lemma pvs_always_r E1 E2 P Q `{!AlwaysStable Q} :
-  (pvs E1 E2 P ∧ Q) ⊑ pvs E1 E2 (P ∧ Q).
+  ((|={E1,E2}=> P) ∧ Q) ⊑ (|={E1,E2}=> P ∧ Q).
 Proof. by rewrite !always_and_sep_r pvs_frame_r. Qed.
-Lemma pvs_impl_l E1 E2 P Q : (□ (P → Q) ∧ pvs E1 E2 P) ⊑ pvs E1 E2 Q.
+Lemma pvs_impl_l E1 E2 P Q : (□ (P → Q) ∧ (|={E1,E2}=> P)) ⊑ (|={E1,E2}=> Q).
 Proof. by rewrite pvs_always_l always_elim impl_elim_l. Qed.
-Lemma pvs_impl_r E1 E2 P Q : (pvs E1 E2 P ∧ □ (P → Q)) ⊑ pvs E1 E2 Q.
+Lemma pvs_impl_r E1 E2 P Q : ((|={E1,E2}=> P) ∧ □ (P → Q)) ⊑ (|={E1,E2}=> Q).
 Proof. by rewrite comm pvs_impl_l. Qed.
 Lemma pvs_wand_l E1 E2 P Q R :
-  P ⊑ pvs E1 E2 Q → ((Q -★ R) ★ P) ⊑ pvs E1 E2 R.
+  P ⊑ (|={E1,E2}=> Q) → ((Q -★ R) ★ P) ⊑ (|={E1,E2}=> R).
 Proof. intros ->. rewrite pvs_frame_l. apply pvs_mono, wand_elim_l. Qed.
 Lemma pvs_wand_r E1 E2 P Q R :
-  P ⊑ pvs E1 E2 Q → (P ★ (Q -★ R)) ⊑ pvs E1 E2 R.
+  P ⊑ (|={E1,E2}=> Q) → (P ★ (Q -★ R)) ⊑ (|={E1,E2}=> R).
 Proof. rewrite comm. apply pvs_wand_l. Qed.
 
 Lemma pvs_mask_frame' E1 E1' E2 E2' P :
-  E1' ⊆ E1 → E2' ⊆ E2 → E1 ∖ E1' = E2 ∖ E2' → pvs E1' E2' P ⊑ pvs E1 E2 P.
+  E1' ⊆ E1 → E2' ⊆ E2 → E1 ∖ E1' = E2 ∖ E2' →
+  (|={E1',E2'}=> P) ⊑ (|={E1,E2}=> P).
 Proof.
   intros HE1 HE2 HEE.
   rewrite (pvs_mask_frame _ _ (E1 ∖ E1')); last set_solver.
   by rewrite {2}HEE -!union_difference_L.
-Qed. 
+Qed.
 
 Lemma pvs_mask_frame_mono E1 E1' E2 E2' P Q :
   E1' ⊆ E1 → E2' ⊆ E2 → E1 ∖ E1' = E2 ∖ E2' →
-  P ⊑ Q → pvs E1' E2' P ⊑ pvs E1 E2 Q.
+  P ⊑ Q → (|={E1',E2'}=> P) ⊑ (|={E1,E2}=> Q).
 Proof. intros HE1 HE2 HEE ->. by apply pvs_mask_frame'. Qed.
 
 (** It should be possible to give a stronger version of this rule
@@ -172,13 +180,13 @@ Proof. intros HE1 HE2 HEE ->. by apply pvs_mask_frame'. Qed.
    mask becomes really ugly then, and we have not found an instance
    where that would be useful. *)
 Lemma pvs_trans3 E1 E2 Q :
-  E2 ⊆ E1 → pvs E1 E2 (pvs E2 E2 (pvs E2 E1 Q)) ⊑ pvs E1 E1 Q.
+  E2 ⊆ E1 → (|={E1,E2}=> |={E2}=> |={E2,E1}=> Q) ⊑ (|={E1}=> Q).
 Proof. intros HE. rewrite !pvs_trans; set_solver. Qed.
 
-Lemma pvs_mask_weaken E1 E2 P : E1 ⊆ E2 → pvs E1 E1 P ⊑ pvs E2 E2 P.
+Lemma pvs_mask_weaken E1 E2 P : E1 ⊆ E2 → (|={E1}=> P) ⊑ (|={E2}=> P).
 Proof. auto using pvs_mask_frame'. Qed.
 
-Lemma pvs_ownG_update E m m' : m ~~> m' → ownG m ⊑ pvs E E (ownG m').
+Lemma pvs_ownG_update E m m' : m ~~> m' → ownG m ⊑ (|={E}=> ownG m').
 Proof.
   intros; rewrite (pvs_ownG_updateP E _ (m' =)); last by apply cmra_update_updateP.
   by apply pvs_mono, uPred.exist_elim=> m''; apply uPred.const_elim_l=> ->.
@@ -195,9 +203,9 @@ Notation FSA Λ Σ A := (coPset → (A → iProp Λ Σ) → iProp Λ Σ).
 Class FrameShiftAssertion {Λ Σ A} (fsaV : Prop) (fsa : FSA Λ Σ A) := {
   fsa_mask_frame_mono E1 E2 Φ Ψ :
     E1 ⊆ E2 → (∀ a, Φ a ⊑ Ψ a) → fsa E1 Φ ⊑ fsa E2 Ψ;
-  fsa_trans3 E Φ : pvs E E (fsa E (λ a, pvs E E (Φ a))) ⊑ fsa E Φ;
+  fsa_trans3 E Φ : (|={E}=> fsa E (λ a, |={E}=> Φ a)) ⊑ fsa E Φ;
   fsa_open_close E1 E2 Φ :
-    fsaV → E2 ⊆ E1 → pvs E1 E2 (fsa E2 (λ a, pvs E2 E1 (Φ a))) ⊑ fsa E1 Φ;
+    fsaV → E2 ⊆ E1 → (|={E1,E2}=> fsa E2 (λ a, |={E2,E1}=> Φ a)) ⊑ fsa E1 Φ;
   fsa_frame_r E P Φ : (fsa E Φ ★ P) ⊑ fsa E (λ a, Φ a ★ P)
 }.
 
@@ -211,16 +219,16 @@ Lemma fsa_mask_weaken E1 E2 Φ : E1 ⊆ E2 → fsa E1 Φ ⊑ fsa E2 Φ.
 Proof. intros. apply fsa_mask_frame_mono; auto. Qed.
 Lemma fsa_frame_l E P Φ : (P ★ fsa E Φ) ⊑ fsa E (λ a, P ★ Φ a).
 Proof. rewrite comm fsa_frame_r. apply fsa_mono=>a. by rewrite comm. Qed.
-Lemma fsa_strip_pvs E P Φ : P ⊑ fsa E Φ → pvs E E P ⊑ fsa E Φ.
+Lemma fsa_strip_pvs E P Φ : P ⊑ fsa E Φ → (|={E}=> P) ⊑ fsa E Φ.
 Proof.
   move=>->. rewrite -{2}fsa_trans3.
   apply pvs_mono, fsa_mono=>a; apply pvs_intro.
 Qed.
-Lemma fsa_mono_pvs E Φ Ψ : (∀ a, Φ a ⊑ pvs E E (Ψ a)) → fsa E Φ ⊑ fsa E Ψ.
+Lemma fsa_mono_pvs E Φ Ψ : (∀ a, Φ a ⊑ (|={E}=> Ψ a)) → fsa E Φ ⊑ fsa E Ψ.
 Proof. intros. rewrite -[fsa E Ψ]fsa_trans3 -pvs_intro. by apply fsa_mono. Qed.
 End fsa.
 
-Definition pvs_fsa {Λ Σ} : FSA Λ Σ () := λ E Φ, pvs E E (Φ ()).
+Definition pvs_fsa {Λ Σ} : FSA Λ Σ () := λ E Φ, (|={E}=> Φ ())%I.
 Instance pvs_fsa_prf {Λ Σ} : FrameShiftAssertion True (@pvs_fsa Λ Σ).
 Proof.
   rewrite /pvs_fsa.
diff --git a/program_logic/resources.v b/program_logic/resources.v
index 28781d2b46013c183d888653da84ba046b523d31..f3d1ed208ec4be04ec1b01c5b30aaf8278bc2f0b 100644
--- a/program_logic/resources.v
+++ b/program_logic/resources.v
@@ -84,14 +84,14 @@ Lemma res_included (r1 r2 : res Λ Σ A) :
   r1 ≼ r2 ↔ wld r1 ≼ wld r2 ∧ pst r1 ≼ pst r2 ∧ gst r1 ≼ gst r2.
 Proof.
   split; [|by intros ([w ?]&[σ ?]&[m ?]); exists (Res w σ m)].
-  intros [r Hr]; split_ands;
+  intros [r Hr]; split_and?;
     [exists (wld r)|exists (pst r)|exists (gst r)]; apply Hr.
 Qed.
 Lemma res_includedN (r1 r2 : res Λ Σ A) n :
   r1 ≼{n} r2 ↔ wld r1 ≼{n} wld r2 ∧ pst r1 ≼{n} pst r2 ∧ gst r1 ≼{n} gst r2.
 Proof.
   split; [|by intros ([w ?]&[σ ?]&[m ?]); exists (Res w σ m)].
-  intros [r Hr]; split_ands;
+  intros [r Hr]; split_and?;
     [exists (wld r)|exists (pst r)|exists (gst r)]; apply Hr.
 Qed.
 Definition res_cmra_mixin : CMRAMixin (res Λ Σ A).
@@ -99,18 +99,18 @@ Proof.
   split.
   - by intros n x [???] ? [???]; constructor; simpl in *; cofe_subst.
   - by intros n [???] ? [???]; constructor; simpl in *; cofe_subst.
-  - by intros n [???] ? [???] (?&?&?); split_ands'; simpl in *; cofe_subst.
+  - by intros n [???] ? [???] (?&?&?); split_and!; simpl in *; cofe_subst.
   - by intros n [???] ? [???] [???] ? [???];
       constructor; simpl in *; cofe_subst.
-  - by intros n ? (?&?&?); split_ands'; apply cmra_validN_S.
+  - by intros n ? (?&?&?); split_and!; apply cmra_validN_S.
   - by intros ???; constructor; rewrite /= assoc.
   - by intros ??; constructor; rewrite /= comm.
   - by intros ?; constructor; rewrite /= cmra_unit_l.
   - by intros ?; constructor; rewrite /= cmra_unit_idemp.
   - intros n r1 r2; rewrite !res_includedN.
-    by intros (?&?&?); split_ands'; apply cmra_unit_preservingN.
+    by intros (?&?&?); split_and!; apply cmra_unit_preservingN.
   - intros n r1 r2 (?&?&?);
-      split_ands'; simpl in *; eapply cmra_validN_op_l; eauto.
+      split_and!; simpl in *; eapply cmra_validN_op_l; eauto.
   - intros n r1 r2; rewrite res_includedN; intros (?&?&?).
     by constructor; apply cmra_op_minus.
 Qed.
@@ -127,7 +127,7 @@ Canonical Structure resRA : cmraT :=
 Global Instance res_cmra_identity : CMRAIdentity resRA.
 Proof.
   split.
-  - intros n; split_ands'; apply cmra_empty_valid.
+  - intros n; split_and!; apply cmra_empty_valid.
   - by split; rewrite /= left_id.
   - apply _.
 Qed.
@@ -205,8 +205,8 @@ Instance res_map_cmra_monotone {Λ Σ} {A B : cofeT} (f : A -n> B) :
 Proof.
   split.
   - by intros n r1 r2; rewrite !res_includedN;
-      intros (?&?&?); split_ands'; simpl; try apply includedN_preserving.
-  - by intros n r (?&?&?); split_ands'; simpl; try apply validN_preserving.
+      intros (?&?&?); split_and!; simpl; try apply includedN_preserving.
+  - by intros n r (?&?&?); split_and!; simpl; try apply validN_preserving.
 Qed.
 Definition resC_map {Λ Σ A B} (f : A -n> B) : resC Λ Σ A -n> resC Λ Σ B :=
   CofeMor (res_map f : resRA Λ Σ A → resRA Λ Σ B).
diff --git a/program_logic/sts.v b/program_logic/sts.v
index db5f5f9d2f05011256300d3214bec3fbddba5c5b..5bfca1f2957272d5635907e41bd70bedb2ce99d4 100644
--- a/program_logic/sts.v
+++ b/program_logic/sts.v
@@ -42,8 +42,8 @@ Section sts.
   Proof. by intros φ1 φ2 Hφ; rewrite /sts_inv; setoid_rewrite Hφ. Qed.
   Global Instance sts_ownS_proper γ : Proper ((≡) ==> (≡) ==> (≡)) (sts_ownS γ).
   Proof. intros S1 S2 HS T1 T2 HT. by rewrite /sts_ownS HS HT. Qed.
-  Global Instance sts_own_proper γ s : Proper ((≡) ==> (≡)) (sts_ownS γ s).
-  Proof. intros T1 T2 HT. by rewrite /sts_ownS HT. Qed.
+  Global Instance sts_own_proper γ s : Proper ((≡) ==> (≡)) (sts_own γ s).
+  Proof. intros T1 T2 HT. by rewrite /sts_own HT. Qed.
   Global Instance sts_ctx_ne n γ N :
     Proper (pointwise_relation _ (dist n) ==> dist n) (sts_ctx γ N).
   Proof. by intros φ1 φ2 Hφ; rewrite /sts_ctx Hφ. Qed.
@@ -55,14 +55,13 @@ Section sts.
      sts_frag_included. *)
   Lemma sts_ownS_weaken E γ S1 S2 T1 T2 :
     T1 ≡ T2 → S1 ⊆ S2 → sts.closed S2 T2 →
-    sts_ownS γ S1 T1 ⊑ pvs E E (sts_ownS γ S2 T2).
+    sts_ownS γ S1 T1 ⊑ (|={E}=> sts_ownS γ S2 T2).
   Proof. intros -> ? ?. by apply own_update, sts_update_frag. Qed.
 
   Lemma sts_own_weaken E γ s S T1 T2 :
     T1 ≡ T2 → s ∈ S → sts.closed S T2 →
-    sts_own γ s T1 ⊑ pvs E E (sts_ownS γ S T2).
-  (* FIXME for some reason, using "->" instead of "<-" does not work? *)
-  Proof. intros <- ? ?. by apply own_update, sts_update_frag_up. Qed.
+    sts_own γ s T1 ⊑ (|={E}=> sts_ownS γ S T2).
+  Proof. intros -> ??. by apply own_update, sts_update_frag_up. Qed.
 
   Lemma sts_ownS_op γ S1 S2 T1 T2 :
     T1 ∩ T2 ⊆ ∅ → sts.closed S1 T1 → sts.closed S2 T2 →
@@ -71,7 +70,7 @@ Section sts.
 
   Lemma sts_alloc E N s :
     nclose N ⊆ E →
-    ▷ φ s ⊑ pvs E E (∃ γ, sts_ctx γ N φ ∧ sts_own γ s (⊤ ∖ sts.tok s)).
+    ▷ φ s ⊑ (|={E}=> ∃ γ, sts_ctx γ N φ ∧ sts_own γ s (⊤ ∖ sts.tok s)).
   Proof.
     intros HN. eapply sep_elim_True_r.
     { apply (own_alloc (sts_auth s (⊤ ∖ sts.tok s)) N).
@@ -89,7 +88,7 @@ Section sts.
 
   Lemma sts_opened E γ S T :
     (▷ sts_inv γ φ ★ sts_ownS γ S T)
-    ⊑ pvs E E (∃ s, ■ (s ∈ S) ★ ▷ φ s ★ own γ (sts_auth s T)).
+    ⊑ (|={E}=> ∃ s, ■ (s ∈ S) ★ ▷ φ s ★ own γ (sts_auth s T)).
   Proof.
     rewrite /sts_inv /sts_ownS later_exist sep_exist_r. apply exist_elim=>s.
     rewrite later_sep pvs_timeless !pvs_frame_r. apply pvs_mono.
@@ -105,13 +104,13 @@ Section sts.
 
   Lemma sts_closing E γ s T s' T' :
     sts.step (s, T) (s', T') →
-    (▷ φ s' ★ own γ (sts_auth s T)) ⊑ pvs E E (▷ sts_inv γ φ ★ sts_own γ s' T').
+    (▷ φ s' ★ own γ (sts_auth s T)) ⊑ (|={E}=> ▷ sts_inv γ φ ★ sts_own γ s' T').
   Proof.
     intros Hstep. rewrite /sts_inv /sts_own -(exist_intro s').
     rewrite later_sep [(_ ★ ▷φ _)%I]comm -assoc.
     rewrite -pvs_frame_l. apply sep_mono_r. rewrite -later_intro.
     rewrite own_valid_l discrete_validI. apply const_elim_sep_l=>Hval.
-    transitivity (pvs E E (own γ (sts_auth s' T'))).
+    transitivity (|={E}=> own γ (sts_auth s' T'))%I.
     { by apply own_update, sts_update_auth. }
     by rewrite -own_op sts_op_auth_frag_up; last by inversion_clear Hstep.
   Qed.
diff --git a/program_logic/viewshifts.v b/program_logic/viewshifts.v
index 7656044e9583bbd8a9218a908bda641bdeccdd27..8ed30859e70e5e229f6121eee33986c6c5bfb0a8 100644
--- a/program_logic/viewshifts.v
+++ b/program_logic/viewshifts.v
@@ -3,26 +3,26 @@ From program_logic Require Export pviewshifts invariants ghost_ownership.
 Import uPred.
 
 Definition vs {Λ Σ} (E1 E2 : coPset) (P Q : iProp Λ Σ) : iProp Λ Σ :=
-  (□ (P → pvs E1 E2 Q))%I.
+  (□ (P → |={E1,E2}=> Q))%I.
 Arguments vs {_ _} _ _ _%I _%I.
 Instance: Params (@vs) 4.
 Notation "P ={ E1 , E2 }=> Q" := (vs E1 E2 P%I Q%I)
-  (at level 199, E1 at level 1, E2 at level 1,
+  (at level 199, E1,E2 at level 50,
    format "P  ={ E1 , E2 }=>  Q") : uPred_scope.
 Notation "P ={ E1 , E2 }=> Q" := (True ⊑ vs E1 E2 P%I Q%I)
-  (at level 199, E1 at level 1, E2 at level 1,
+  (at level 199, E1, E2 at level 50,
    format "P  ={ E1 , E2 }=>  Q") : C_scope.
 Notation "P ={ E }=> Q" := (vs E E P%I Q%I)
-  (at level 199, E at level 1, format "P  ={ E }=>  Q") : uPred_scope.
+  (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 1, format "P  ={ E }=>  Q") : C_scope.
+  (at level 199, E at level 50, format "P  ={ E }=>  Q") : C_scope.
 
 Section vs.
 Context {Λ : language} {Σ : iFunctor}.
 Implicit Types P Q R : iProp Λ Σ.
 Implicit Types N : namespace.
 
-Lemma vs_alt E1 E2 P Q : (P ⊑ pvs E1 E2 Q) → P ={E1,E2}=> Q.
+Lemma vs_alt E1 E2 P Q : P ⊑ (|={E1,E2}=> Q) → P ={E1,E2}=> Q.
 Proof.
   intros; rewrite -{1}always_const. apply: always_intro. apply impl_intro_l.
   by rewrite always_const right_id.
diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index 45297039316250ce925dc37fbad752eccc684908..28f4f2ac7352672af8f34d624c4656a7c7069536 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -21,7 +21,7 @@ Record wp_go {Λ Σ} (E : coPset) (Φ Φfork : expr Λ → nat → iRes Λ Σ 
 }.
 CoInductive wp_pre {Λ Σ} (E : coPset)
      (Φ : val Λ → iProp Λ Σ) : expr Λ → nat → iRes Λ Σ → Prop :=
-  | wp_pre_value n r v : pvs E E (Φ v) n r → wp_pre E Φ (of_val v) n r
+  | wp_pre_value n r v : (|={E}=> Φ v)%I n r → wp_pre E Φ (of_val v) n r
   | wp_pre_step n r1 e1 :
      to_val e1 = None →
      (∀ rf k Ef σ1,
@@ -46,11 +46,18 @@ Next Obligation.
     destruct (Hgo (rf' ⋅ rf) k Ef σ1) as [Hsafe Hstep];
       rewrite ?assoc -?Hr; auto; constructor; [done|].
     intros e2 σ2 ef ?; destruct (Hstep e2 σ2 ef) as (r2&r2'&?&?&?); auto.
-    exists r2, (r2' â‹… rf'); split_ands; eauto 10 using (IH k), cmra_included_l.
+    exists r2, (r2' â‹… rf'); split_and?; eauto 10 using (IH k), cmra_included_l.
     by rewrite -!assoc (assoc _ r2).
 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 Λ Σ.
@@ -73,7 +80,7 @@ Proof.
   destruct (Hgo rf k Ef σ1) as [Hsafe Hstep]; auto.
   split; [done|intros e2 σ2 ef ?].
   destruct (Hstep e2 σ2 ef) as (r2&r2'&?&?&?); auto.
-  exists r2, r2'; split_ands; [|eapply IH|]; eauto.
+  exists r2, r2'; split_and?; [|eapply IH|]; eauto.
 Qed.
 Global Instance wp_proper E e :
   Proper (pointwise_relation _ (≡) ==> (≡)) (@wp Λ Σ E e).
@@ -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].
@@ -92,22 +99,23 @@ Proof.
   destruct (Hgo rf k ((E2 ∖ E1) ∪ Ef) σ1) as [Hsafe Hstep]; rewrite -?HE'; auto.
   split; [done|intros e2 σ2 ef ?].
   destruct (Hstep e2 σ2 ef) as (r2&r2'&?&?&?); auto.
-  exists r2, r2'; split_ands; [rewrite HE'|eapply IH|]; eauto.
+  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 → pvs E E (Φ v) 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 Φ : pvs 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, pvs E 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|].
@@ -126,10 +134,11 @@ Proof.
   destruct (wp_step_inv E Ef (pvs E E ∘ Φ) e k n σ1 r rf) as [? Hstep]; auto.
   split; [done|intros e2 σ2 ef ?].
   destruct (Hstep e2 σ2 ef) as (r2&r2'&?&Hwp'&?); auto.
-  exists r2, r2'; split_ands; [|apply (IH k)|]; auto.
+  exists r2, r2'; split_and?; [|apply (IH k)|]; auto.
 Qed.
 Lemma wp_atomic E1 E2 e Φ :
-  E2 ⊆ E1 → atomic e → pvs E1 E2 (wp E2 e (λ v, pvs 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 ???.
@@ -142,11 +151,11 @@ Proof.
     [|destruct (atomic_step e σ1 e2 σ2 ef); naive_solver].
   apply pvs_trans in Hvs'; auto.
   destruct (Hvs' (r2' ⋅ rf) k Ef σ2) as (r3&[]); rewrite ?assoc; auto.
-  exists r3, r2'; split_ands; last done.
+  exists r3, r2'; split_and?; last done.
   - 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.
@@ -158,13 +167,13 @@ Proof.
   { by rewrite assoc. }
   split; [done|intros e2 σ2 ef ?].
   destruct (Hstep e2 σ2 ef) as (r2&r2'&?&?&?); auto.
-  exists (r2 â‹… rR), r2'; split_ands; auto.
+  exists (r2 â‹… rR), r2'; split_and?; auto.
   - by rewrite -(assoc _ r2)
       (comm _ rR) !assoc -(assoc _ _ rR).
   - 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|].
@@ -172,13 +181,13 @@ Proof.
   destruct (Hgo (rR⋅rf) k Ef σ1) as [Hsafe Hstep];rewrite ?assoc;auto.
   split; [done|intros e2 σ2 ef ?].
   destruct (Hstep e2 σ2 ef) as (r2&r2'&?&?&?); auto.
-  exists (r2 â‹… rR), r2'; split_ands; auto.
+  exists (r2 â‹… rR), r2'; split_and?; auto.
   - by rewrite -(assoc _ r2) (comm _ rR) !assoc -(assoc _ _ rR).
-  - apply wp_frame_r; [auto|exists r2, rR; split_ands; auto].
+  - apply wp_frame_r; [auto|exists r2, rR; split_and?; auto].
     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|].
@@ -190,45 +199,50 @@ Proof.
   intros e2 σ2 ef ?.
   destruct (fill_step_inv e σ1 e2 σ2 ef) as (e2'&->&?); auto.
   destruct (Hstep e2' σ2 ef) as (r2&r2'&?&?&?); auto.
-  exists r2, r2'; split_ands; try eapply IH; eauto.
+  exists r2, r2'; split_and?; try eapply IH; eauto.
 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 Φ → pvs 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 → pvs E 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. *)
diff --git a/program_logic/wsat.v b/program_logic/wsat.v
index 5795b16e2dcbcc12f3d71bbe4cf126dc5f148293..2e9da973fa7fa0b58637fb8ad546c074c0ebfcce 100644
--- a/program_logic/wsat.v
+++ b/program_logic/wsat.v
@@ -72,7 +72,7 @@ Lemma wsat_init k E σ mm : ✓{S k} mm → wsat (S k) E σ (Res ∅ (Excl σ) m
 Proof.
   intros Hv. exists ∅; constructor; auto.
   - rewrite big_opM_empty right_id.
-    split_ands'; try (apply cmra_valid_validN, ra_empty_valid);
+    split_and!; try (apply cmra_valid_validN, ra_empty_valid);
       constructor || apply Hv.
   - by intros i; rewrite lookup_empty=>-[??].
   - intros i P ?; rewrite /= left_id lookup_empty; inversion_clear 1.
@@ -123,7 +123,7 @@ Proof.
     apply (inj Excl).
     by rewrite -Hpst_r -Hpst -assoc Hpst' right_id. }
   split; [done|exists rs].
-  by constructor; split_ands'; try (rewrite /= -assoc Hpst').
+  by constructor; first split_and!; try rewrite /= -assoc Hpst'.
 Qed.
 Lemma wsat_update_gst n E σ r rf mm1 (P : iGst Λ Σ → Prop) :
   mm1 ≼{S n} gst r → mm1 ~~>: (λ mm2, default False mm2 P) →
@@ -132,7 +132,8 @@ Proof.
   intros [mf Hr] Hup [rs [(?&?&?) Hσ HE Hwld]].
   destruct (Hup (S n) (mf â‹… gst (rf â‹… big_opM rs))) as ([m2|]&?&Hval'); try done.
   { by rewrite /= (assoc _ mm1) -Hr assoc. }
-  exists m2; split; [exists rs; split; split_ands'; auto|done].
+  exists m2; split; [exists rs|done].
+  by constructor; first split_and!; auto.
 Qed.
 Lemma wsat_alloc n E1 E2 σ r P rP :
   ¬set_finite E1 → P n rP → wsat (S n) (E1 ∪ E2) σ (rP ⋅ r) →
@@ -153,9 +154,9 @@ Proof.
     rewrite /= !lookup_op !op_is_Some -!not_eq_None_Some; tauto. }
   assert (r ⋅ big_opM (<[i:=rP]> rs) ≡ rP ⋅ r ⋅ big_opM rs) as Hr.
   { by rewrite (comm _ rP) -assoc big_opM_insert. }
-  exists i; split_ands; [exists (<[i:=rP]>rs); constructor| |]; auto.
+  exists i; split_and?; [exists (<[i:=rP]>rs); constructor| |]; auto.
   - destruct Hval as (?&?&?);  rewrite -assoc Hr.
-    split_ands'; rewrite /= ?left_id; [|eauto|eauto].
+    split_and!; rewrite /= ?left_id; [|eauto|eauto].
     intros j; destruct (decide (j = i)) as [->|].
     + by rewrite !lookup_op Hri HrPi Hrsi !right_id lookup_singleton.
     + by rewrite lookup_op lookup_singleton_ne // left_id.