diff --git a/algebra/agree.v b/algebra/agree.v
index 320b7ae1e4847aeebf5cb7fac55ed63745a91672..6479419c0d202ed1d2d02664592cb5c03a5c8579 100644
--- a/algebra/agree.v
+++ b/algebra/agree.v
@@ -136,7 +136,7 @@ Lemma to_agree_car n (x : agree A) : ✓{n} x → to_agree (x n) ≡{n}≡ x.
 Proof. intros [??]; split; naive_solver eauto using agree_valid_le. Qed.
 
 (** Internalized properties *)
-Lemma agree_equivI {M} a b : (to_agree a ≡ to_agree b) ⊣⊢ (a ≡ b : uPred M).
+Lemma agree_equivI {M} a b : to_agree a ≡ to_agree b ⊣⊢ (a ≡ b : uPred M).
 Proof.
   uPred.unseal. do 2 split. by intros [? Hv]; apply (Hv n). apply: to_agree_ne.
 Qed.
diff --git a/algebra/auth.v b/algebra/auth.v
index 366e852310c02e8523896a78655c22ccdac0898b..e974e056f0a8f3c74a3052d8a6652e2a2f36867e 100644
--- a/algebra/auth.v
+++ b/algebra/auth.v
@@ -164,14 +164,14 @@ Canonical Structure authUR :=
 
 (** Internalized properties *)
 Lemma auth_equivI {M} (x y : auth A) :
-  (x ≡ y) ⊣⊢ (authoritative x ≡ authoritative y ∧ own x ≡ own y : uPred M).
+  x ≡ y ⊣⊢ (authoritative x ≡ authoritative y ∧ own x ≡ own y : uPred M).
 Proof. by uPred.unseal. Qed.
 Lemma auth_validI {M} (x : auth A) :
-  (✓ x) ⊣⊢ (match authoritative x with
-             | Excl' a => (∃ b, a ≡ own x ⋅ b) ∧ ✓ a
-             | None => ✓ own x
-             | ExclBot' => False
-             end : uPred M).
+  ✓ x ⊣⊢ (match authoritative x with
+          | Excl' a => (∃ b, a ≡ own x ⋅ b) ∧ ✓ a
+          | None => ✓ own x
+          | ExclBot' => False
+          end : uPred M).
 Proof. uPred.unseal. by destruct x as [[[]|]]. Qed.
 
 Lemma auth_frag_op a b : ◯ (a ⋅ b) ≡ ◯ a ⋅ ◯ b.
diff --git a/algebra/csum.v b/algebra/csum.v
index 45ce720bd79b27e34e5562e16b6b2b383dce5f34..9fdedfcd286f951a84427cc9b648a57452d2cf5f 100644
--- a/algebra/csum.v
+++ b/algebra/csum.v
@@ -236,22 +236,22 @@ Proof. rewrite /Persistent /=. inversion_clear 1; by repeat constructor. Qed.
 
 (** Internalized properties *)
 Lemma csum_equivI {M} (x y : csum A B) :
-  (x ≡ y) ⊣⊢ (match x, y with
-               | Cinl a, Cinl a' => a ≡ a'
-               | Cinr b, Cinr b' => b ≡ b'
-               | CsumBot, CsumBot => True
-               | _, _ => False
-               end : uPred M).
+  x ≡ y ⊣⊢ (match x, y with
+            | Cinl a, Cinl a' => a ≡ a'
+            | Cinr b, Cinr b' => b ≡ b'
+            | CsumBot, CsumBot => True
+            | _, _ => False
+            end : uPred M).
 Proof.
   uPred.unseal; do 2 split; first by destruct 1.
   by destruct x, y; try destruct 1; try constructor.
 Qed.
 Lemma csum_validI {M} (x : csum A B) :
-  (✓ x) ⊣⊢ (match x with
-            | Cinl a => ✓ a
-            | Cinr b => ✓ b
-            | CsumBot => False
-            end : uPred M).
+  ✓ x ⊣⊢ (match x with
+          | Cinl a => ✓ a
+          | Cinr b => ✓ b
+          | CsumBot => False
+          end : uPred M).
 Proof. uPred.unseal. by destruct x. Qed.
 
 (** Updates *)
diff --git a/algebra/excl.v b/algebra/excl.v
index c67a912fabbcc6157369e752d167074cb2f36c61..3eaf1181e00ec4b23b927be5607b409ccee0a89e 100644
--- a/algebra/excl.v
+++ b/algebra/excl.v
@@ -102,11 +102,11 @@ Proof. split. apply _. by intros []. Qed.
 
 (** Internalized properties *)
 Lemma excl_equivI {M} (x y : excl A) :
-  (x ≡ y) ⊣⊢ (match x, y with
-               | Excl a, Excl b => a ≡ b
-               | ExclBot, ExclBot => True
-               | _, _ => False
-               end : uPred M).
+  x ≡ y ⊣⊢ (match x, y with
+            | Excl a, Excl b => a ≡ b
+            | ExclBot, ExclBot => True
+            | _, _ => False
+            end : uPred M).
 Proof.
   uPred.unseal. do 2 split. by destruct 1. by destruct x, y; try constructor.
 Qed.
diff --git a/algebra/frac.v b/algebra/frac.v
index 6581ce2534a0d5926a2290f0089c4f73d6b00860..8b3018f8841652b32e63cd10ab627d17bd63177b 100644
--- a/algebra/frac.v
+++ b/algebra/frac.v
@@ -153,7 +153,7 @@ Proof. intros. by apply frac_validN_inv_l with 0 y, cmra_valid_validN. Qed.
 
 (** Internalized properties *)
 Lemma frac_equivI {M} (x y : frac A) :
-  (x ≡ y) ⊣⊢ (frac_perm x = frac_perm y ∧ frac_car x ≡ frac_car y : uPred M).
+  x ≡ y ⊣⊢ (frac_perm x = frac_perm y ∧ frac_car x ≡ frac_car y : uPred M).
 Proof. by uPred.unseal. Qed.
 Lemma frac_validI {M} (x : frac A) :
   ✓ x ⊣⊢ (■ (frac_perm x ≤ 1)%Qc ∧ ✓ frac_car x : uPred M).
diff --git a/algebra/gmap.v b/algebra/gmap.v
index 6753711e0498f8bbab908666d9787212604aafcb..36cd9bbcdef1bea85ba0da8c5dd51dcbe41ce40a 100644
--- a/algebra/gmap.v
+++ b/algebra/gmap.v
@@ -171,9 +171,9 @@ Canonical Structure gmapUR :=
   UCMRAT (gmap K A) gmap_cofe_mixin gmap_cmra_mixin gmap_ucmra_mixin.
 
 (** Internalized properties *)
-Lemma gmap_equivI {M} m1 m2 : (m1 ≡ m2) ⊣⊢ (∀ i, m1 !! i ≡ m2 !! i : uPred M).
+Lemma gmap_equivI {M} m1 m2 : m1 ≡ m2 ⊣⊢ (∀ i, m1 !! i ≡ m2 !! i : uPred M).
 Proof. by uPred.unseal. Qed.
-Lemma gmap_validI {M} m : (✓ m) ⊣⊢ (∀ i, ✓ (m !! i) : uPred M).
+Lemma gmap_validI {M} m : ✓ m ⊣⊢ (∀ i, ✓ (m !! i) : uPred M).
 Proof. by uPred.unseal. Qed.
 End cmra.
 
diff --git a/algebra/iprod.v b/algebra/iprod.v
index ecb2ac1cae3587fab8ede88576105c9b122b72b6..26cdb338fe7f4c177305d06193b211c6613501f9 100644
--- a/algebra/iprod.v
+++ b/algebra/iprod.v
@@ -139,9 +139,9 @@ Section iprod_cmra.
     UCMRAT (iprod B) iprod_cofe_mixin iprod_cmra_mixin iprod_ucmra_mixin.
 
   (** Internalized properties *)
-  Lemma iprod_equivI {M} g1 g2 : (g1 ≡ g2) ⊣⊢ (∀ i, g1 i ≡ g2 i : uPred M).
+  Lemma iprod_equivI {M} g1 g2 : g1 ≡ g2 ⊣⊢ (∀ i, g1 i ≡ g2 i : uPred M).
   Proof. by uPred.unseal. Qed.
-  Lemma iprod_validI {M} g : (✓ g) ⊣⊢ (∀ i, ✓ g i : uPred M).
+  Lemma iprod_validI {M} g : ✓ g ⊣⊢ (∀ i, ✓ g i : uPred M).
   Proof. by uPred.unseal. Qed.
 
   (** Properties of iprod_insert. *)
diff --git a/algebra/list.v b/algebra/list.v
index 17f9b32ff847c601cde5be2484cf6fa9468e26be..183514da98b33a3c2e236661fe6cdf3a02b78d7a 100644
--- a/algebra/list.v
+++ b/algebra/list.v
@@ -227,9 +227,9 @@ Section cmra.
   Qed.
 
   (** Internalized properties *)
-  Lemma list_equivI {M} l1 l2 : (l1 ≡ l2) ⊣⊢ (∀ i, l1 !! i ≡ l2 !! i : uPred M).
+  Lemma list_equivI {M} l1 l2 : l1 ≡ l2 ⊣⊢ (∀ i, l1 !! i ≡ l2 !! i : uPred M).
   Proof. uPred.unseal; constructor=> n x ?. apply list_dist_lookup. Qed.
-  Lemma list_validI {M} l : (✓ l) ⊣⊢ (∀ i, ✓ (l !! i) : uPred M).
+  Lemma list_validI {M} l : ✓ l ⊣⊢ (∀ i, ✓ (l !! i) : uPred M).
   Proof. uPred.unseal; constructor=> n x ?. apply list_lookup_validN. Qed.
 End cmra.
 
diff --git a/algebra/one_shot.v b/algebra/one_shot.v
index 5c3f6f6a0c510d7e25261f902a2d71eb9c849bb0..c2344ec7ff11c66b0cd9bf891285f92a74465142 100644
--- a/algebra/one_shot.v
+++ b/algebra/one_shot.v
@@ -196,22 +196,22 @@ Proof. rewrite /Persistent /=. inversion_clear 1; by repeat constructor. Qed.
 
 (** Internalized properties *)
 Lemma one_shot_equivI {M} (x y : one_shot A) :
-  (x ≡ y) ⊣⊢ (match x, y with
-               | OneShotPending, OneShotPending => True
-               | Shot a, Shot b => a ≡ b
-               | OneShotBot, OneShotBot => True
-               | _, _ => False
-               end : uPred M).
+  x ≡ y ⊣⊢ (match x, y with
+            | OneShotPending, OneShotPending => True
+            | Shot a, Shot b => a ≡ b
+            | OneShotBot, OneShotBot => True
+            | _, _ => False
+            end : uPred M).
 Proof.
   uPred.unseal; do 2 split; first by destruct 1.
   by destruct x, y; try destruct 1; try constructor.
 Qed.
 Lemma one_shot_validI {M} (x : one_shot A) :
-  (✓ x) ⊣⊢ (match x with
-            | Shot a => ✓ a 
-            | OneShotBot => False
-            | _ => True
-            end : uPred M).
+  ✓ x ⊣⊢ (match x with
+          | Shot a => ✓ a 
+          | OneShotBot => False
+          | _ => True
+          end : uPred M).
 Proof. uPred.unseal. by destruct x. Qed.
 
 (** Updates *)
diff --git a/algebra/upred.v b/algebra/upred.v
index 33a7afb0a8904588e3e217c821067bfe5e12ac6a..f513350d5a264892712f98a909d05647067a4de5 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -257,9 +257,11 @@ Definition uPred_valid {M A} := proj1_sig uPred_valid_aux M A.
 Definition uPred_valid_eq :
   @uPred_valid = @uPred_valid_def := proj2_sig uPred_valid_aux.
 
-Notation "P ⊢ Q" := (uPred_entails P%I Q%I) (at level 70) : C_scope.
+Notation "P ⊢ Q" := (uPred_entails P%I Q%I)
+  (at level 99, Q at level 200, right associativity) : C_scope.
 Notation "(⊢)" := uPred_entails (only parsing) : C_scope.
-Notation "P ⊣⊢ Q" := (equiv (A:=uPred _) P%I Q%I) (at level 70) : C_scope.
+Notation "P ⊣⊢ Q" := (equiv (A:=uPred _) P%I Q%I)
+  (at level 95, no associativity) : C_scope.
 Notation "(⊣⊢)" := (equiv (A:=uPred _)) (only parsing) : C_scope.
 Notation "■ φ" := (uPred_const φ%C%type)
   (at level 20, right associativity) : uPred_scope.
@@ -329,14 +331,14 @@ Proof.
 Qed.
 Global Instance: AntiSymm (⊣⊢) (@uPred_entails M).
 Proof. intros P Q HPQ HQP; split=> x n; by split; [apply HPQ|apply HQP]. Qed.
-Lemma equiv_spec P Q : P ⊣⊢ Q ↔ P ⊢ Q ∧ Q ⊢ P.
+Lemma equiv_spec P Q : (P ⊣⊢ Q) ↔ (P ⊢ Q) ∧ (Q ⊢ P).
 Proof.
   split; [|by intros [??]; apply (anti_symm (⊢))].
   intros HPQ; split; split=> x i; apply HPQ.
 Qed.
-Lemma equiv_entails P Q : P ⊣⊢ Q → P ⊢ Q.
+Lemma equiv_entails P Q : (P ⊣⊢ Q) → (P ⊢ Q).
 Proof. apply equiv_spec. Qed.
-Lemma equiv_entails_sym P Q : Q ⊣⊢ P → P ⊢ Q.
+Lemma equiv_entails_sym P Q : (Q ⊣⊢ P) → (P ⊢ Q).
 Proof. apply equiv_spec. Qed.
 Global Instance entails_proper :
   Proper ((⊣⊢) ==> (⊣⊢) ==> iff) ((⊢) : relation (uPred M)).
@@ -345,9 +347,9 @@ Proof.
   - by trans P1; [|trans Q1].
   - by trans P2; [|trans Q2].
 Qed.
-Lemma entails_equiv_l (P Q R : uPred M) : P ⊣⊢ Q → Q ⊢ R → P ⊢ R.
+Lemma entails_equiv_l (P Q R : uPred M) : (P ⊣⊢ Q) → (Q ⊢ R) → (P ⊢ R).
 Proof. by intros ->. Qed.
-Lemma entails_equiv_r (P Q R : uPred M) : P ⊢ Q → Q ⊣⊢ R → P ⊢ R.
+Lemma entails_equiv_r (P Q R : uPred M) : (P ⊢ Q) → (Q ⊣⊢ R) → (P ⊢ R).
 Proof. by intros ? <-. Qed.
 
 (** Non-expansiveness and setoid morphisms *)
@@ -459,53 +461,53 @@ Global Instance iff_proper :
 (** Introduction and elimination rules *)
 Lemma const_intro φ P : φ → P ⊢ ■ φ.
 Proof. by intros ?; unseal; split. Qed.
-Lemma const_elim φ Q R : Q ⊢ ■ φ → (φ → Q ⊢ R) → Q ⊢ R.
+Lemma const_elim φ Q R : (Q ⊢ ■ φ) → (φ → Q ⊢ R) → Q ⊢ R.
 Proof.
   unseal; intros HQP HQR; split=> n x ??; apply HQR; first eapply HQP; eauto.
 Qed.
-Lemma and_elim_l P Q : (P ∧ Q) ⊢ P.
+Lemma and_elim_l P Q : P ∧ Q ⊢ P.
 Proof. by unseal; split=> n x ? [??]. Qed.
-Lemma and_elim_r P Q : (P ∧ Q) ⊢ Q.
+Lemma and_elim_r P Q : P ∧ Q ⊢ Q.
 Proof. by unseal; split=> n x ? [??]. Qed.
-Lemma and_intro P Q R : P ⊢ Q → P ⊢ R → P ⊢ (Q ∧ R).
+Lemma and_intro P Q R : (P ⊢ Q) → (P ⊢ R) → P ⊢ Q ∧ R.
 Proof. intros HQ HR; unseal; split=> n x ??; by split; [apply HQ|apply HR]. Qed.
-Lemma or_intro_l P Q : P ⊢ (P ∨ Q).
+Lemma or_intro_l P Q : P ⊢ P ∨ Q.
 Proof. unseal; split=> n x ??; left; auto. Qed.
-Lemma or_intro_r P Q : Q ⊢ (P ∨ Q).
+Lemma or_intro_r P Q : Q ⊢ P ∨ Q.
 Proof. unseal; split=> n x ??; right; auto. Qed.
-Lemma or_elim P Q R : P ⊢ R → Q ⊢ R → (P ∨ Q) ⊢ R.
+Lemma or_elim P Q R : (P ⊢ R) → (Q ⊢ R) → P ∨ Q ⊢ R.
 Proof. intros HP HQ; unseal; split=> n x ? [?|?]. by apply HP. by apply HQ. Qed.
-Lemma impl_intro_r P Q R : (P ∧ Q) ⊢ R → P ⊢ (Q → R).
+Lemma impl_intro_r P Q R : (P ∧ Q ⊢ R) → P ⊢ Q → R.
 Proof.
   unseal; intros HQ; split=> n x ?? n' x' ????. apply HQ;
     naive_solver eauto using uPred_mono, uPred_closed, cmra_included_includedN.
 Qed.
-Lemma impl_elim P Q R : P ⊢ (Q → R) → P ⊢ Q → P ⊢ R.
+Lemma impl_elim P Q R : (P ⊢ Q → R) → (P ⊢ Q) → P ⊢ R.
 Proof. by unseal; intros HP HP'; split=> n x ??; apply HP with n x, HP'. Qed.
-Lemma forall_intro {A} P (Ψ : A → uPred M): (∀ a, P ⊢ Ψ a) → P ⊢ (∀ a, Ψ a).
+Lemma forall_intro {A} P (Ψ : A → uPred M): (∀ a, P ⊢ Ψ a) → P ⊢ ∀ a, Ψ a.
 Proof. unseal; intros HPΨ; split=> n x ?? a; by apply HPΨ. Qed.
 Lemma forall_elim {A} {Ψ : A → uPred M} a : (∀ a, Ψ a) ⊢ Ψ a.
 Proof. unseal; split=> n x ? HP; apply HP. Qed.
-Lemma exist_intro {A} {Ψ : A → uPred M} a : Ψ a ⊢ (∃ a, Ψ a).
+Lemma exist_intro {A} {Ψ : A → uPred M} a : Ψ a ⊢ ∃ a, Ψ a.
 Proof. unseal; split=> n x ??; by exists a. Qed.
 Lemma exist_elim {A} (Φ : A → uPred M) Q : (∀ a, Φ a ⊢ Q) → (∃ a, Φ a) ⊢ Q.
 Proof. unseal; intros HΦΨ; split=> n x ? [a ?]; by apply HΦΨ with a. Qed.
-Lemma eq_refl {A : cofeT} (a : A) : True ⊢ (a ≡ a).
+Lemma eq_refl {A : cofeT} (a : A) : True ⊢ a ≡ a.
 Proof. unseal; by split=> n x ??; simpl. Qed.
 Lemma eq_rewrite {A : cofeT} a b (Ψ : A → uPred M) P
-  {HΨ : ∀ n, Proper (dist n ==> dist n) Ψ} : P ⊢ (a ≡ b) → P ⊢ Ψ a → P ⊢ Ψ b.
+  {HΨ : ∀ n, Proper (dist n ==> dist n) Ψ} : (P ⊢ a ≡ b) → (P ⊢ Ψ a) → P ⊢ Ψ b.
 Proof.
   unseal; intros Hab Ha; split=> n x ??. apply HΨ with n a; auto.
   - by symmetry; apply Hab with x.
   - by apply Ha.
 Qed.
-Lemma eq_equiv {A : cofeT} (a b : A) : True ⊢ (a ≡ b) → a ≡ b.
+Lemma eq_equiv {A : cofeT} (a b : A) : (True ⊢ a ≡ b) → a ≡ b.
 Proof.
   unseal=> Hab; apply equiv_dist; intros n; apply Hab with ∅; last done.
   apply cmra_valid_validN, ucmra_unit_valid.
 Qed.
 Lemma eq_rewrite_contractive {A : cofeT} a b (Ψ : A → uPred M) P
-  {HΨ : Contractive Ψ} : P ⊢ ▷ (a ≡ b) → P ⊢ Ψ a → P ⊢ Ψ b.
+  {HΨ : Contractive Ψ} : (P ⊢ ▷ (a ≡ b)) → (P ⊢ Ψ a) → P ⊢ Ψ b.
 Proof.
   unseal; intros Hab Ha; split=> n x ??. apply HΨ with n a; auto.
   - destruct n; intros m ?; first omega. apply (dist_le n); last omega.
@@ -518,74 +520,74 @@ Lemma False_elim P : False ⊢ P.
 Proof. by apply (const_elim False). Qed.
 Lemma True_intro P : P ⊢ True.
 Proof. by apply const_intro. Qed.
-Lemma and_elim_l' P Q R : P ⊢ R → (P ∧ Q) ⊢ R.
+Lemma and_elim_l' P Q R : (P ⊢ R) → P ∧ Q ⊢ R.
 Proof. by rewrite and_elim_l. Qed.
-Lemma and_elim_r' P Q R : Q ⊢ R → (P ∧ Q) ⊢ R.
+Lemma and_elim_r' P Q R : (Q ⊢ R) → P ∧ Q ⊢ R.
 Proof. by rewrite and_elim_r. Qed.
-Lemma or_intro_l' P Q R : P ⊢ Q → P ⊢ (Q ∨ R).
+Lemma or_intro_l' P Q R : (P ⊢ Q) → P ⊢ Q ∨ R.
 Proof. intros ->; apply or_intro_l. Qed.
-Lemma or_intro_r' P Q R : P ⊢ R → P ⊢ (Q ∨ R).
+Lemma or_intro_r' P Q R : (P ⊢ R) → P ⊢ Q ∨ R.
 Proof. intros ->; apply or_intro_r. Qed.
-Lemma exist_intro' {A} P (Ψ : A → uPred M) a : P ⊢ Ψ a → P ⊢ (∃ a, Ψ a).
+Lemma exist_intro' {A} P (Ψ : A → uPred M) a : (P ⊢ Ψ a) → P ⊢ ∃ a, Ψ a.
 Proof. intros ->; apply exist_intro. Qed.
-Lemma forall_elim' {A} P (Ψ : A → uPred M) : P ⊢ (∀ a, Ψ a) → (∀ a, P ⊢ Ψ a).
+Lemma forall_elim' {A} P (Ψ : A → uPred M) : (P ⊢ ∀ a, Ψ a) → ∀ a, P ⊢ Ψ a.
 Proof. move=> HP a. by rewrite HP forall_elim. Qed.
 
 Hint Resolve or_elim or_intro_l' or_intro_r'.
 Hint Resolve and_intro and_elim_l' and_elim_r'.
 Hint Immediate True_intro False_elim.
 
-Lemma impl_intro_l P Q R : (Q ∧ P) ⊢ R → P ⊢ (Q → R).
+Lemma impl_intro_l P Q R : (Q ∧ P ⊢ R) → P ⊢ Q → R.
 Proof. intros HR; apply impl_intro_r; rewrite -HR; auto. Qed.
-Lemma impl_elim_l P Q : ((P → Q) ∧ P) ⊢ Q.
+Lemma impl_elim_l P Q : (P → Q) ∧ P ⊢ Q.
 Proof. apply impl_elim with P; auto. Qed.
-Lemma impl_elim_r P Q : (P ∧ (P → Q)) ⊢ Q.
+Lemma impl_elim_r P Q : P ∧ (P → Q) ⊢ Q.
 Proof. apply impl_elim with P; auto. Qed.
-Lemma impl_elim_l' P Q R : P ⊢ (Q → R) → (P ∧ Q) ⊢ R.
+Lemma impl_elim_l' P Q R : (P ⊢ Q → R) → P ∧ Q ⊢ R.
 Proof. intros; apply impl_elim with Q; auto. Qed.
-Lemma impl_elim_r' P Q R : Q ⊢ (P → R) → (P ∧ Q) ⊢ R.
+Lemma impl_elim_r' P Q R : (Q ⊢ P → R) → P ∧ Q ⊢ R.
 Proof. intros; apply impl_elim with P; auto. Qed.
-Lemma impl_entails P Q : True ⊢ (P → Q) → P ⊢ Q.
+Lemma impl_entails P Q : (True ⊢ P → Q) → P ⊢ Q.
 Proof. intros HPQ; apply impl_elim with P; rewrite -?HPQ; auto. Qed.
-Lemma entails_impl P Q : (P ⊢ Q) → True ⊢ (P → Q).
+Lemma entails_impl P Q : (P ⊢ Q) → True ⊢ P → Q.
 Proof. auto using impl_intro_l. Qed.
 
-Lemma iff_refl Q P : Q ⊢ (P ↔ P).
+Lemma iff_refl Q P : Q ⊢ P ↔ P.
 Proof. rewrite /uPred_iff; apply and_intro; apply impl_intro_l; auto. Qed.
-Lemma iff_equiv P Q : True ⊢ (P ↔ Q) → P ⊣⊢ Q.
+Lemma iff_equiv P Q : (True ⊢ P ↔ Q) → (P ⊣⊢ Q).
 Proof.
   intros HPQ; apply (anti_symm (⊢));
     apply impl_entails; rewrite HPQ /uPred_iff; auto.
 Qed.
-Lemma equiv_iff P Q : P ⊣⊢ Q → True ⊢ (P ↔ Q).
+Lemma equiv_iff P Q : (P ⊣⊢ Q) → True ⊢ P ↔ Q.
 Proof. intros ->; apply iff_refl. Qed.
 
 Lemma const_mono φ1 φ2 : (φ1 → φ2) → ■ φ1 ⊢ ■ φ2.
 Proof. intros; apply const_elim with φ1; eauto using const_intro. Qed.
-Lemma and_mono P P' Q Q' : P ⊢ Q → P' ⊢ Q' → (P ∧ P') ⊢ (Q ∧ Q').
+Lemma and_mono P P' Q Q' : (P ⊢ Q) → (P' ⊢ Q') → P ∧ P' ⊢ Q ∧ Q'.
 Proof. auto. Qed.
-Lemma and_mono_l P P' Q : P ⊢ Q → (P ∧ P') ⊢ (Q ∧ P').
+Lemma and_mono_l P P' Q : (P ⊢ Q) → P ∧ P' ⊢ Q ∧ P'.
 Proof. by intros; apply and_mono. Qed.
-Lemma and_mono_r P P' Q' : P' ⊢ Q' → (P ∧ P') ⊢ (P ∧ Q').
+Lemma and_mono_r P P' Q' : (P' ⊢ Q') → P ∧ P' ⊢ P ∧ Q'.
 Proof. by apply and_mono. Qed.
-Lemma or_mono P P' Q Q' : P ⊢ Q → P' ⊢ Q' → (P ∨ P') ⊢ (Q ∨ Q').
+Lemma or_mono P P' Q Q' : (P ⊢ Q) → (P' ⊢ Q') → P ∨ P' ⊢ Q ∨ Q'.
 Proof. auto. Qed.
-Lemma or_mono_l P P' Q : P ⊢ Q → (P ∨ P') ⊢ (Q ∨ P').
+Lemma or_mono_l P P' Q : (P ⊢ Q) → P ∨ P' ⊢ Q ∨ P'.
 Proof. by intros; apply or_mono. Qed.
-Lemma or_mono_r P P' Q' : P' ⊢ Q' → (P ∨ P') ⊢ (P ∨ Q').
+Lemma or_mono_r P P' Q' : (P' ⊢ Q') → P ∨ P' ⊢ P ∨ Q'.
 Proof. by apply or_mono. Qed.
-Lemma impl_mono P P' Q Q' : Q ⊢ P → P' ⊢ Q' → (P → P') ⊢ (Q → Q').
+Lemma impl_mono P P' Q Q' : (Q ⊢ P) → (P' ⊢ Q') → (P → P') ⊢ Q → Q'.
 Proof.
   intros HP HQ'; apply impl_intro_l; rewrite -HQ'.
   apply impl_elim with P; eauto.
 Qed.
 Lemma forall_mono {A} (Φ Ψ : A → uPred M) :
-  (∀ a, Φ a ⊢ Ψ a) → (∀ a, Φ a) ⊢ (∀ a, Ψ a).
+  (∀ a, Φ a ⊢ Ψ a) → (∀ a, Φ a) ⊢ ∀ a, Ψ a.
 Proof.
   intros HP. apply forall_intro=> a; rewrite -(HP a); apply forall_elim.
 Qed.
 Lemma exist_mono {A} (Φ Ψ : A → uPred M) :
-  (∀ a, Φ a ⊢ Ψ a) → (∃ a, Φ a) ⊢ (∃ a, Ψ a).
+  (∀ a, Φ a ⊢ Ψ a) → (∃ a, Φ a) ⊢ ∃ a, Ψ a.
 Proof. intros HΦ. apply exist_elim=> a; rewrite (HΦ a); apply exist_intro. Qed.
 Global Instance const_mono' : Proper (impl ==> (⊢)) (@uPred_const M).
 Proof. intros φ1 φ2; apply const_mono. Qed.
@@ -644,21 +646,21 @@ Proof.
   - by apply impl_intro_l; rewrite left_id.
 Qed.
 
-Lemma or_and_l P Q R : (P ∨ Q ∧ R) ⊣⊢ ((P ∨ Q) ∧ (P ∨ R)).
+Lemma or_and_l P Q R : P ∨ Q ∧ R ⊣⊢ (P ∨ Q) ∧ (P ∨ R).
 Proof.
   apply (anti_symm (⊢)); first auto.
   do 2 (apply impl_elim_l', or_elim; apply impl_intro_l); auto.
 Qed.
-Lemma or_and_r P Q R : (P ∧ Q ∨ R) ⊣⊢ ((P ∨ R) ∧ (Q ∨ R)).
+Lemma or_and_r P Q R : P ∧ Q ∨ R ⊣⊢ (P ∨ R) ∧ (Q ∨ R).
 Proof. by rewrite -!(comm _ R) or_and_l. Qed.
-Lemma and_or_l P Q R : (P ∧ (Q ∨ R)) ⊣⊢ (P ∧ Q ∨ P ∧ R).
+Lemma and_or_l P Q R : P ∧ (Q ∨ R) ⊣⊢ P ∧ Q ∨ P ∧ R.
 Proof.
   apply (anti_symm (⊢)); last auto.
   apply impl_elim_r', or_elim; apply impl_intro_l; auto.
 Qed.
-Lemma and_or_r P Q R : ((P ∨ Q) ∧ R) ⊣⊢ (P ∧ R ∨ Q ∧ R).
+Lemma and_or_r P Q R : (P ∨ Q) ∧ R ⊣⊢ P ∧ R ∨ Q ∧ R.
 Proof. by rewrite -!(comm _ R) and_or_l. Qed.
-Lemma and_exist_l {A} P (Ψ : A → uPred M) : (P ∧ ∃ a, Ψ a) ⊣⊢ (∃ a, P ∧ Ψ a).
+Lemma and_exist_l {A} P (Ψ : A → uPred M) : P ∧ (∃ a, Ψ a) ⊣⊢ ∃ a, P ∧ Ψ a.
 Proof.
   apply (anti_symm (⊢)).
   - apply impl_elim_r'. apply exist_elim=>a. apply impl_intro_l.
@@ -666,38 +668,38 @@ Proof.
   - apply exist_elim=>a. apply and_intro; first by rewrite and_elim_l.
     by rewrite -(exist_intro a) and_elim_r.
 Qed.
-Lemma and_exist_r {A} P (Φ: A → uPred M) : ((∃ a, Φ a) ∧ P) ⊣⊢ (∃ a, Φ a ∧ P).
+Lemma and_exist_r {A} P (Φ: A → uPred M) : (∃ a, Φ a) ∧ P ⊣⊢ ∃ a, Φ a ∧ P.
 Proof.
   rewrite -(comm _ P) and_exist_l. apply exist_proper=>a. by rewrite comm.
 Qed.
 
-Lemma const_intro_l φ Q R : φ → (■ φ ∧ Q) ⊢ R → Q ⊢ R.
+Lemma const_intro_l φ Q R : φ → (■ φ ∧ Q ⊢ R) → Q ⊢ R.
 Proof. intros ? <-; auto using const_intro. Qed.
-Lemma const_intro_r φ Q R : φ → (Q ∧ ■ φ) ⊢ R → Q ⊢ R.
+Lemma const_intro_r φ Q R : φ → (Q ∧ ■ φ ⊢ R) → Q ⊢ R.
 Proof. intros ? <-; auto using const_intro. Qed.
-Lemma const_intro_impl φ Q R : φ → Q ⊢ (■ φ → R) → Q ⊢ R.
+Lemma const_intro_impl φ Q R : φ → (Q ⊢ ■ φ → R) → Q ⊢ R.
 Proof. intros ? ->. eauto using const_intro_l, impl_elim_r. Qed.
-Lemma const_elim_l φ Q R : (φ → Q ⊢ R) → (■ φ ∧ Q) ⊢ R.
+Lemma const_elim_l φ Q R : (φ → Q ⊢ R) → ■ φ ∧ Q ⊢ R.
 Proof. intros; apply const_elim with φ; eauto. Qed.
-Lemma const_elim_r φ Q R : (φ → Q ⊢ R) → (Q ∧ ■ φ) ⊢ R.
+Lemma const_elim_r φ Q R : (φ → Q ⊢ R) → Q ∧ ■ φ ⊢ R.
 Proof. intros; apply const_elim with φ; eauto. Qed.
-Lemma const_equiv (φ : Prop) : φ → (■ φ) ⊣⊢ True.
+Lemma const_equiv (φ : Prop) : φ → ■ φ ⊣⊢ True.
 Proof. intros; apply (anti_symm _); auto using const_intro. Qed.
 
-Lemma eq_refl' {A : cofeT} (a : A) P : P ⊢ (a ≡ a).
+Lemma eq_refl' {A : cofeT} (a : A) P : P ⊢ a ≡ a.
 Proof. rewrite (True_intro P). apply eq_refl. Qed.
 Hint Resolve eq_refl'.
-Lemma equiv_eq {A : cofeT} P (a b : A) : a ≡ b → P ⊢ (a ≡ b).
+Lemma equiv_eq {A : cofeT} P (a b : A) : a ≡ b → P ⊢ a ≡ b.
 Proof. by intros ->. Qed.
-Lemma eq_sym {A : cofeT} (a b : A) : (a ≡ b) ⊢ (b ≡ a).
+Lemma eq_sym {A : cofeT} (a b : A) : a ≡ b ⊢ b ≡ a.
 Proof. apply (eq_rewrite a b (λ b, b ≡ a)%I); auto. solve_proper. Qed.
-Lemma eq_iff P Q : (P ≡ Q) ⊢ (P ↔ Q).
+Lemma eq_iff P Q : P ≡ Q ⊢ P ↔ Q.
 Proof.
   apply (eq_rewrite P Q (λ Q, P ↔ Q))%I; first solve_proper; auto using iff_refl.
 Qed.
 
 (* BI connectives *)
-Lemma sep_mono P P' Q Q' : P ⊢ Q → P' ⊢ Q' → (P ★ P') ⊢ (Q ★ Q').
+Lemma sep_mono P P' Q Q' : (P ⊢ Q) → (P' ⊢ Q') → P ★ P' ⊢ Q ★ Q'.
 Proof.
   intros HQ HQ'; unseal.
   split; intros n' x ? (x1&x2&?&?&?); exists x1,x2; cofe_subst x;
@@ -724,13 +726,13 @@ Proof.
     + by rewrite (assoc op) -Hy -Hx.
     + by exists y2, x2.
 Qed.
-Lemma wand_intro_r P Q R : (P ★ Q) ⊢ R → P ⊢ (Q -★ R).
+Lemma wand_intro_r P Q R : (P ★ Q ⊢ R) → P ⊢ Q -★ R.
 Proof.
   unseal=> HPQR; split=> n x ?? n' x' ???; apply HPQR; auto.
   exists x, x'; split_and?; auto.
   eapply uPred_closed with n; eauto using cmra_validN_op_l.
 Qed.
-Lemma wand_elim_l' P Q R : P ⊢ (Q -★ R) → (P ★ Q) ⊢ R.
+Lemma wand_elim_l' P Q R : (P ⊢ Q -★ R) → P ★ Q ⊢ R.
 Proof.
   unseal =>HPQR. split; intros n x ? (?&?&?&?&?). cofe_subst.
   eapply HPQR; eauto using cmra_validN_op_l.
@@ -738,16 +740,16 @@ Qed.
 
 (* Derived BI Stuff *)
 Hint Resolve sep_mono.
-Lemma sep_mono_l P P' Q : P ⊢ Q → (P ★ P') ⊢ (Q ★ P').
+Lemma sep_mono_l P P' Q : (P ⊢ Q) → P ★ P' ⊢ Q ★ P'.
 Proof. by intros; apply sep_mono. Qed.
-Lemma sep_mono_r P P' Q' : P' ⊢ Q' → (P ★ P') ⊢ (P ★ Q').
+Lemma sep_mono_r P P' Q' : (P' ⊢ Q') → P ★ P' ⊢ P ★ Q'.
 Proof. by apply sep_mono. Qed.
 Global Instance sep_mono' : Proper ((⊢) ==> (⊢) ==> (⊢)) (@uPred_sep M).
 Proof. by intros P P' HP Q Q' HQ; apply sep_mono. Qed.
 Global Instance sep_flip_mono' :
   Proper (flip (⊢) ==> flip (⊢) ==> flip (⊢)) (@uPred_sep M).
 Proof. by intros P P' HP Q Q' HQ; apply sep_mono. Qed.
-Lemma wand_mono P P' Q Q' : Q ⊢ P → P' ⊢ Q' → (P -★ P') ⊢ (Q -★ Q').
+Lemma wand_mono P P' Q Q' : (Q ⊢ P) → (P' ⊢ Q') → (P -★ P') ⊢ Q -★ Q'.
 Proof.
   intros HP HQ; apply wand_intro_r. rewrite HP -HQ. by apply wand_elim_l'.
 Qed.
@@ -756,42 +758,42 @@ Proof. by intros P P' HP Q Q' HQ; apply wand_mono. Qed.
 
 Global Instance sep_True : RightId (⊣⊢) True%I (@uPred_sep M).
 Proof. by intros P; rewrite comm left_id. Qed.
-Lemma sep_elim_l P Q : (P ★ Q) ⊢ P.
+Lemma sep_elim_l P Q : P ★ Q ⊢ P.
 Proof. by rewrite (True_intro Q) right_id. Qed.
-Lemma sep_elim_r P Q : (P ★ Q) ⊢ Q.
+Lemma sep_elim_r P Q : P ★ Q ⊢ Q.
 Proof. by rewrite (comm (★))%I; apply sep_elim_l. Qed.
-Lemma sep_elim_l' P Q R : P ⊢ R → (P ★ Q) ⊢ R.
+Lemma sep_elim_l' P Q R : (P ⊢ R) → P ★ Q ⊢ R.
 Proof. intros ->; apply sep_elim_l. Qed.
-Lemma sep_elim_r' P Q R : Q ⊢ R → (P ★ Q) ⊢ R.
+Lemma sep_elim_r' P Q R : (Q ⊢ R) → P ★ Q ⊢ R.
 Proof. intros ->; apply sep_elim_r. Qed.
 Hint Resolve sep_elim_l' sep_elim_r'.
-Lemma sep_intro_True_l P Q R : True ⊢ P → R ⊢ Q → R ⊢ (P ★ Q).
+Lemma sep_intro_True_l P Q R : (True ⊢ P) → (R ⊢ Q) → R ⊢ P ★ Q.
 Proof. by intros; rewrite -(left_id True%I uPred_sep R); apply sep_mono. Qed.
-Lemma sep_intro_True_r P Q R : R ⊢ P → True ⊢ Q → R ⊢ (P ★ Q).
+Lemma sep_intro_True_r P Q R : (R ⊢ P) → (True ⊢ Q) → R ⊢ P ★ Q.
 Proof. by intros; rewrite -(right_id True%I uPred_sep R); apply sep_mono. Qed.
-Lemma sep_elim_True_l P Q R : True ⊢ P → (P ★ R) ⊢ Q → R ⊢ Q.
+Lemma sep_elim_True_l P Q R : (True ⊢ P) → (P ★ R ⊢ Q) → R ⊢ Q.
 Proof. by intros HP; rewrite -HP left_id. Qed.
-Lemma sep_elim_True_r P Q R : True ⊢ P → (R ★ P) ⊢ Q → R ⊢ Q.
+Lemma sep_elim_True_r P Q R : (True ⊢ P) → (R ★ P ⊢ Q) → R ⊢ Q.
 Proof. by intros HP; rewrite -HP right_id. Qed.
-Lemma wand_intro_l P Q R : (Q ★ P) ⊢ R → P ⊢ (Q -★ R).
+Lemma wand_intro_l P Q R : (Q ★ P ⊢ R) → P ⊢ Q -★ R.
 Proof. rewrite comm; apply wand_intro_r. Qed.
-Lemma wand_elim_l P Q : ((P -★ Q) ★ P) ⊢ Q.
+Lemma wand_elim_l P Q : (P -★ Q) ★ P ⊢ Q.
 Proof. by apply wand_elim_l'. Qed.
-Lemma wand_elim_r P Q : (P ★ (P -★ Q)) ⊢ Q.
+Lemma wand_elim_r P Q : P ★ (P -★ Q) ⊢ Q.
 Proof. rewrite (comm _ P); apply wand_elim_l. Qed.
-Lemma wand_elim_r' P Q R : Q ⊢ (P -★ R) → (P ★ Q) ⊢ R.
+Lemma wand_elim_r' P Q R : (Q ⊢ P -★ R) → P ★ Q ⊢ R.
 Proof. intros ->; apply wand_elim_r. Qed.
-Lemma wand_apply_l P Q Q' R R' : P ⊢ (Q' -★ R') → R' ⊢ R → Q ⊢ Q' → (P ★ Q) ⊢ R.
+Lemma wand_apply_l P Q Q' R R' : (P ⊢ Q' -★ R') → (R' ⊢ R) → (Q ⊢ Q') → P ★ Q ⊢ R.
 Proof. intros -> -> <-; apply wand_elim_l. Qed.
-Lemma wand_apply_r P Q Q' R R' : P ⊢ (Q' -★ R') → R' ⊢ R → Q ⊢ Q' → (Q ★ P) ⊢ R.
+Lemma wand_apply_r P Q Q' R R' : (P ⊢ Q' -★ R') → (R' ⊢ R) → (Q ⊢ Q') → Q ★ P ⊢ R.
 Proof. intros -> -> <-; apply wand_elim_r. Qed.
-Lemma wand_apply_l' P Q Q' R : P ⊢ (Q' -★ R) → Q ⊢ Q' → (P ★ Q) ⊢ R.
+Lemma wand_apply_l' P Q Q' R : (P ⊢ Q' -★ R) → (Q ⊢ Q') → P ★ Q ⊢ R.
 Proof. intros -> <-; apply wand_elim_l. Qed.
-Lemma wand_apply_r' P Q Q' R : P ⊢ (Q' -★ R) → Q ⊢ Q' → (Q ★ P) ⊢ R.
+Lemma wand_apply_r' P Q Q' R : (P ⊢ Q' -★ R) → (Q ⊢ Q') → Q ★ P ⊢ R.
 Proof. intros -> <-; apply wand_elim_r. Qed.
-Lemma wand_frame_l P Q R : (Q -★ R) ⊢ (P ★ Q -★ P ★ R).
+Lemma wand_frame_l P Q R : (Q -★ R) ⊢ P ★ Q -★ P ★ R.
 Proof. apply wand_intro_l. rewrite -assoc. apply sep_mono_r, wand_elim_r. Qed.
-Lemma wand_frame_r P Q R : (Q -★ R) ⊢ (Q ★ P -★ R ★ P).
+Lemma wand_frame_r P Q R : (Q -★ R) ⊢ Q ★ P -★ R ★ P.
 Proof.
   apply wand_intro_l. rewrite ![(_ ★ P)%I]comm -assoc.
   apply sep_mono_r, wand_elim_r.
@@ -803,11 +805,11 @@ Proof.
   apply (anti_symm _); last by auto using wand_intro_l.
   eapply sep_elim_True_l; first reflexivity. by rewrite wand_elim_r.
 Qed.
-Lemma wand_entails P Q : True ⊢ (P -★ Q) → P ⊢ Q.
+Lemma wand_entails P Q : (True ⊢ P -★ Q) → P ⊢ Q.
 Proof.
   intros HPQ. eapply sep_elim_True_r; first exact: HPQ. by rewrite wand_elim_r.
 Qed.
-Lemma entails_wand P Q : (P ⊢ Q) → True ⊢ (P -★ Q).
+Lemma entails_wand P Q : (P ⊢ Q) → True ⊢ P -★ Q.
 Proof. auto using wand_intro_l. Qed.
 Lemma wand_curry P Q R : (P -★ Q -★ R) ⊣⊢ (P ★ Q -★ R).
 Proof.
@@ -818,11 +820,11 @@ Qed.
 
 Lemma sep_and P Q : (P ★ Q) ⊢ (P ∧ Q).
 Proof. auto. Qed.
-Lemma impl_wand P Q : (P → Q) ⊢ (P -★ Q).
+Lemma impl_wand P Q : (P → Q) ⊢ P -★ Q.
 Proof. apply wand_intro_r, impl_elim with P; auto. Qed.
-Lemma const_elim_sep_l φ Q R : (φ → Q ⊢ R) → (■ φ ★ Q) ⊢ R.
+Lemma const_elim_sep_l φ Q R : (φ → Q ⊢ R) → ■ φ ★ Q ⊢ R.
 Proof. intros; apply const_elim with φ; eauto. Qed.
-Lemma const_elim_sep_r φ Q R : (φ → Q ⊢ R) → (Q ★ ■ φ) ⊢ R.
+Lemma const_elim_sep_r φ Q R : (φ → Q ⊢ R) → Q ★ ■ φ ⊢ R.
 Proof. intros; apply const_elim with φ; eauto. Qed.
 
 Global Instance sep_False : LeftAbsorb (⊣⊢) False%I (@uPred_sep M).
@@ -830,31 +832,29 @@ Proof. intros P; apply (anti_symm _); auto. Qed.
 Global Instance False_sep : RightAbsorb (⊣⊢) False%I (@uPred_sep M).
 Proof. intros P; apply (anti_symm _); auto. Qed.
 
-Lemma sep_and_l P Q R : (P ★ (Q ∧ R)) ⊢ ((P ★ Q) ∧ (P ★ R)).
+Lemma sep_and_l P Q R : P ★ (Q ∧ R) ⊢ (P ★ Q) ∧ (P ★ R).
 Proof. auto. Qed.
-Lemma sep_and_r P Q R : ((P ∧ Q) ★ R) ⊢ ((P ★ R) ∧ (Q ★ R)).
+Lemma sep_and_r P Q R : (P ∧ Q) ★ R ⊢ (P ★ R) ∧ (Q ★ R).
 Proof. auto. Qed.
-Lemma sep_or_l P Q R : (P ★ (Q ∨ R)) ⊣⊢ ((P ★ Q) ∨ (P ★ R)).
+Lemma sep_or_l P Q R : P ★ (Q ∨ R) ⊣⊢ (P ★ Q) ∨ (P ★ R).
 Proof.
   apply (anti_symm (⊢)); last by eauto 8.
-  apply wand_elim_r', or_elim; apply wand_intro_l.
-  - by apply or_intro_l.
-  - by apply or_intro_r.
+  apply wand_elim_r', or_elim; apply wand_intro_l; auto.
 Qed.
-Lemma sep_or_r P Q R : ((P ∨ Q) ★ R) ⊣⊢ ((P ★ R) ∨ (Q ★ R)).
+Lemma sep_or_r P Q R : (P ∨ Q) ★ R ⊣⊢ (P ★ R) ∨ (Q ★ R).
 Proof. by rewrite -!(comm _ R) sep_or_l. Qed.
-Lemma sep_exist_l {A} P (Ψ : A → uPred M) : (P ★ ∃ a, Ψ a) ⊣⊢ (∃ a, P ★ Ψ a).
+Lemma sep_exist_l {A} P (Ψ : A → uPred M) : P ★ (∃ a, Ψ a) ⊣⊢ ∃ a, P ★ Ψ a.
 Proof.
   intros; apply (anti_symm (⊢)).
   - apply wand_elim_r', exist_elim=>a. apply wand_intro_l.
     by rewrite -(exist_intro a).
   - apply exist_elim=> a; apply sep_mono; auto using exist_intro.
 Qed.
-Lemma sep_exist_r {A} (Φ: A → uPred M) Q: ((∃ a, Φ a) ★ Q) ⊣⊢ (∃ a, Φ a ★ Q).
+Lemma sep_exist_r {A} (Φ: A → uPred M) Q: (∃ a, Φ a) ★ Q ⊣⊢ ∃ a, Φ a ★ Q.
 Proof. setoid_rewrite (comm _ _ Q); apply sep_exist_l. Qed.
-Lemma sep_forall_l {A} P (Ψ : A → uPred M) : (P ★ ∀ a, Ψ a) ⊢ (∀ a, P ★ Ψ a).
+Lemma sep_forall_l {A} P (Ψ : A → uPred M) : P ★ (∀ a, Ψ a) ⊢ ∀ a, P ★ Ψ a.
 Proof. by apply forall_intro=> a; rewrite forall_elim. Qed.
-Lemma sep_forall_r {A} (Φ : A → uPred M) Q : ((∀ a, Φ a) ★ Q) ⊢ (∀ a, Φ a ★ Q).
+Lemma sep_forall_r {A} (Φ : A → uPred M) Q : (∀ a, Φ a) ★ Q ⊢ ∀ a, Φ a ★ Q.
 Proof. by apply forall_intro=> a; rewrite forall_elim. Qed.
 
 (* Always *)
@@ -865,14 +865,14 @@ Proof.
   unseal; split=> n x ? /=.
   eauto using uPred_mono, @cmra_included_core, cmra_included_includedN.
 Qed.
-Lemma always_intro' P Q : □ P ⊢ Q → □ P ⊢ □ Q.
+Lemma always_intro' P Q : (□ P ⊢ Q) → □ P ⊢ □ Q.
 Proof.
   unseal=> HPQ; split=> n x ??; apply HPQ; simpl; auto using @cmra_core_validN.
   by rewrite cmra_core_idemp.
 Qed.
-Lemma always_and P Q : □ (P ∧ Q) ⊣⊢ (□ P ∧ □ Q).
+Lemma always_and P Q : □ (P ∧ Q) ⊣⊢ □ P ∧ □ Q.
 Proof. by unseal. Qed.
-Lemma always_or P Q : □ (P ∨ Q) ⊣⊢ (□ P ∨ □ Q).
+Lemma always_or P Q : □ (P ∨ Q) ⊣⊢ □ P ∨ □ Q.
 Proof. by unseal. Qed.
 Lemma always_forall {A} (Ψ : A → uPred M) : (□ ∀ a, Ψ a) ⊣⊢ (∀ a, □ Ψ a).
 Proof. by unseal. Qed.
@@ -883,7 +883,7 @@ Proof.
   unseal; split=> n x ? [??].
   exists (core x), (core x); rewrite -cmra_core_dup; auto.
 Qed.
-Lemma always_and_sep_l_1 P Q : (□ P ∧ Q) ⊢ (□ P ★ Q).
+Lemma always_and_sep_l_1 P Q : □ P ∧ Q ⊢ □ P ★ Q.
 Proof.
   unseal; split=> n x ? [??]; exists (core x), x; simpl in *.
   by rewrite cmra_core_l cmra_core_idemp.
@@ -892,7 +892,7 @@ Lemma always_later P : □ ▷ P ⊣⊢ ▷ □ P.
 Proof. by unseal. Qed.
 
 (* Always derived *)
-Lemma always_mono P Q : P ⊢ Q → □ P ⊢ □ Q.
+Lemma always_mono P Q : (P ⊢ Q) → □ P ⊢ □ Q.
 Proof. intros. apply always_intro'. by rewrite always_elim. Qed.
 Hint Resolve always_mono.
 Global Instance always_mono' : Proper ((⊢) ==> (⊢)) (@uPred_always M).
@@ -900,12 +900,12 @@ Proof. intros P Q; apply always_mono. Qed.
 Global Instance always_flip_mono' :
   Proper (flip (⊢) ==> flip (⊢)) (@uPred_always M).
 Proof. intros P Q; apply always_mono. Qed.
-Lemma always_impl P Q : □ (P → Q) ⊢ (□ P → □ Q).
+Lemma always_impl P Q : □ (P → Q) ⊢ □ P → □ Q.
 Proof.
   apply impl_intro_l; rewrite -always_and.
   apply always_mono, impl_elim with P; auto.
 Qed.
-Lemma always_eq {A:cofeT} (a b : A) : □ (a ≡ b) ⊣⊢ (a ≡ b).
+Lemma always_eq {A:cofeT} (a b : A) : □ (a ≡ b) ⊣⊢ a ≡ b.
 Proof.
   apply (anti_symm (⊢)); auto using always_elim.
   apply (eq_rewrite a b (λ b, □ (a ≡ b))%I); auto.
@@ -914,15 +914,15 @@ Proof.
 Qed.
 Lemma always_and_sep P Q : □ (P ∧ Q) ⊣⊢ □ (P ★ Q).
 Proof. apply (anti_symm (⊢)); auto using always_and_sep_1. Qed.
-Lemma always_and_sep_l' P Q : (□ P ∧ Q) ⊣⊢ (□ P ★ Q).
+Lemma always_and_sep_l' P Q : □ P ∧ Q ⊣⊢ □ P ★ Q.
 Proof. apply (anti_symm (⊢)); auto using always_and_sep_l_1. Qed.
-Lemma always_and_sep_r' P Q : (P ∧ □ Q) ⊣⊢ (P ★ □ Q).
+Lemma always_and_sep_r' P Q : P ∧ □ Q ⊣⊢ P ★ □ Q.
 Proof. by rewrite !(comm _ P) always_and_sep_l'. Qed.
-Lemma always_sep P Q : □ (P ★ Q) ⊣⊢ (□ P ★ □ Q).
+Lemma always_sep P Q : □ (P ★ Q) ⊣⊢ □ P ★ □ Q.
 Proof. by rewrite -always_and_sep -always_and_sep_l' always_and. Qed.
-Lemma always_wand P Q : □ (P -★ Q) ⊢ (□ P -★ □ Q).
+Lemma always_wand P Q : □ (P -★ Q) ⊢ □ P -★ □ Q.
 Proof. by apply wand_intro_r; rewrite -always_sep wand_elim_l. Qed.
-Lemma always_sep_dup' P : □ P ⊣⊢ (□ P ★ □ P).
+Lemma always_sep_dup' P : □ P ⊣⊢ □ P ★ □ P.
 Proof. by rewrite -always_sep -always_and_sep (idemp _). Qed.
 Lemma always_wand_impl P Q : □ (P -★ Q) ⊣⊢ □ (P → Q).
 Proof.
@@ -930,9 +930,9 @@ Proof.
   apply always_intro', impl_intro_r.
   by rewrite always_and_sep_l' always_elim wand_elim_l.
 Qed.
-Lemma always_entails_l' P Q : (P ⊢ □ Q) → P ⊢ (□ Q ★ P).
+Lemma always_entails_l' P Q : (P ⊢ □ Q) → P ⊢ □ Q ★ P.
 Proof. intros; rewrite -always_and_sep_l'; auto. Qed.
-Lemma always_entails_r' P Q : (P ⊢ □ Q) → P ⊢ (P ★ □ Q).
+Lemma always_entails_r' P Q : (P ⊢ □ Q) → P ⊢ P ★ □ Q.
 Proof. intros; rewrite -always_and_sep_r'; auto. Qed.
 
 Global Instance always_if_ne n p : Proper (dist n ==> dist n) (@uPred_always_if M p).
@@ -946,19 +946,19 @@ Lemma always_if_elim p P : □?p P ⊢ P.
 Proof. destruct p; simpl; auto using always_elim. Qed.
 Lemma always_elim_if p P : □ P ⊢ □?p P.
 Proof. destruct p; simpl; auto using always_elim. Qed.
-Lemma always_if_and p P Q : □?p (P ∧ Q) ⊣⊢ (□?p P ∧ □?p Q).
+Lemma always_if_and p P Q : □?p (P ∧ Q) ⊣⊢ □?p P ∧ □?p Q.
 Proof. destruct p; simpl; auto using always_and. Qed.
-Lemma always_if_or p P Q : □?p (P ∨ Q) ⊣⊢ (□?p P ∨ □?p Q).
+Lemma always_if_or p P Q : □?p (P ∨ Q) ⊣⊢ □?p P ∨ □?p Q.
 Proof. destruct p; simpl; auto using always_or. Qed.
-Lemma always_if_exist {A} p (Ψ : A → uPred M) : (□?p ∃ a, Ψ a) ⊣⊢ (∃ a, □?p Ψ a).
+Lemma always_if_exist {A} p (Ψ : A → uPred M) : (□?p ∃ a, Ψ a) ⊣⊢ ∃ a, □?p Ψ a.
 Proof. destruct p; simpl; auto using always_exist. Qed.
-Lemma always_if_sep p P Q : □?p (P ★ Q) ⊣⊢ (□?p P ★ □?p Q).
+Lemma always_if_sep p P Q : □?p (P ★ Q) ⊣⊢ □?p P ★ □?p Q.
 Proof. destruct p; simpl; auto using always_sep. Qed.
-Lemma always_if_later p P : (□?p ▷ P) ⊣⊢ (▷ □?p P).
+Lemma always_if_later p P : □?p ▷ P ⊣⊢ ▷ □?p P.
 Proof. destruct p; simpl; auto using always_later. Qed.
 
 (* Later *)
-Lemma later_mono P Q : P ⊢ Q → ▷ P ⊢ ▷ Q.
+Lemma later_mono P Q : (P ⊢ Q) → ▷ P ⊢ ▷ Q.
 Proof.
   unseal=> HP; split=>-[|n] x ??; [done|apply HP; eauto using cmra_validN_S].
 Qed.
@@ -972,18 +972,17 @@ Proof.
   unseal; split=> n x ? HP; induction n as [|n IH]; [by apply HP|].
   apply HP, IH, uPred_closed with (S n); eauto using cmra_validN_S.
 Qed.
-Lemma later_and P Q : ▷ (P ∧ Q) ⊣⊢ (▷ P ∧ ▷ Q).
+Lemma later_and P Q : ▷ (P ∧ Q) ⊣⊢ ▷ P ∧ ▷ Q.
 Proof. unseal; split=> -[|n] x; by split. Qed.
-Lemma later_or P Q : ▷ (P ∨ Q) ⊣⊢ (▷ P ∨ ▷ Q).
+Lemma later_or P Q : ▷ (P ∨ Q) ⊣⊢ ▷ P ∨ ▷ Q.
 Proof. unseal; split=> -[|n] x; simpl; tauto. Qed.
 Lemma later_forall {A} (Φ : A → uPred M) : (▷ ∀ a, Φ a) ⊣⊢ (∀ a, ▷ Φ a).
 Proof. unseal; by split=> -[|n] x. Qed.
 Lemma later_exist_1 {A} (Φ : A → uPred M) : (∃ a, ▷ Φ a) ⊢ (▷ ∃ a, Φ a).
 Proof. unseal; by split=> -[|[|n]] x. Qed.
-Lemma later_exist' `{Inhabited A} (Φ : A → uPred M) :
-  (▷ ∃ a, Φ a)%I ⊢ (∃ a, ▷ Φ a)%I.
+Lemma later_exist' `{Inhabited A} (Φ : A → uPred M) : (▷ ∃ a, Φ a) ⊢ ∃ a, ▷ Φ a.
 Proof. unseal; split=> -[|[|n]] x; done || by exists inhabitant. Qed.
-Lemma later_sep P Q : ▷ (P ★ Q) ⊣⊢ (▷ P ★ ▷ Q).
+Lemma later_sep P Q : ▷ (P ★ Q) ⊣⊢ ▷ P ★ ▷ Q.
 Proof.
   unseal; split=> n x ?; split.
   - destruct n as [|n]; simpl.
@@ -1003,22 +1002,22 @@ Global Instance later_flip_mono' :
 Proof. intros P Q; apply later_mono. Qed.
 Lemma later_True : ▷ True ⊣⊢ True.
 Proof. apply (anti_symm (⊢)); auto using later_intro. Qed.
-Lemma later_impl P Q : ▷ (P → Q) ⊢ (▷ P → ▷ Q).
+Lemma later_impl P Q : ▷ (P → Q) ⊢ ▷ P → ▷ Q.
 Proof.
   apply impl_intro_l; rewrite -later_and.
   apply later_mono, impl_elim with P; auto.
 Qed.
 Lemma later_exist `{Inhabited A} (Φ : A → uPred M) :
-  (▷ ∃ a, Φ a) ⊣⊢ (∃ a, ▷ Φ a).
+  ▷ (∃ a, Φ a) ⊣⊢ (∃ a, ▷ Φ a).
 Proof. apply: anti_symm; eauto using later_exist', later_exist_1. Qed.
-Lemma later_wand P Q : ▷ (P -★ Q) ⊢ (▷ P -★ ▷ Q).
+Lemma later_wand P Q : ▷ (P -★ Q) ⊢ ▷ P -★ ▷ Q.
 Proof. apply wand_intro_r;rewrite -later_sep; apply later_mono,wand_elim_l. Qed.
-Lemma later_iff P Q : ▷ (P ↔ Q) ⊢ (▷ P ↔ ▷ Q).
+Lemma later_iff P Q : ▷ (P ↔ Q) ⊢ ▷ P ↔ ▷ Q.
 Proof. by rewrite /uPred_iff later_and !later_impl. Qed.
 
 (* Own *)
 Lemma ownM_op (a1 a2 : M) :
-  uPred_ownM (a1 ⋅ a2) ⊣⊢ (uPred_ownM a1 ★ uPred_ownM a2).
+  uPred_ownM (a1 ⋅ a2) ⊣⊢ uPred_ownM a1 ★ uPred_ownM a2.
 Proof.
   unseal; split=> n x ?; split.
   - intros [z ?]; exists a1, (a2 â‹… z); split; [by rewrite (assoc op)|].
@@ -1046,7 +1045,7 @@ Lemma valid_intro {A : cmraT} (a : A) : ✓ a → True ⊢ ✓ a.
 Proof. unseal=> ?; split=> n x ? _ /=; by apply cmra_valid_validN. Qed.
 Lemma valid_elim {A : cmraT} (a : A) : ¬ ✓{0} a → ✓ a ⊢ False.
 Proof. unseal=> Ha; split=> n x ??; apply Ha, cmra_validN_le with n; auto. Qed.
-Lemma always_valid {A : cmraT} (a : A) : (□ (✓ a)) ⊣⊢ (✓ a).
+Lemma always_valid {A : cmraT} (a : A) : □ ✓ a ⊣⊢ ✓ a.
 Proof. by unseal. Qed.
 Lemma valid_weaken {A : cmraT} (a b : A) : ✓ (a ⋅ b) ⊢ ✓ a.
 Proof. unseal; split=> n x _; apply cmra_validN_op_l. Qed.
@@ -1058,37 +1057,34 @@ Global Instance ownM_mono : Proper (flip (≼) ==> (⊢)) (@uPred_ownM M).
 Proof. intros a b [b' ->]. rewrite ownM_op. eauto. Qed.
 
 (* Products *)
-Lemma prod_equivI {A B : cofeT} (x y : A * B) :
-  (x ≡ y) ⊣⊢ (x.1 ≡ y.1 ∧ x.2 ≡ y.2).
+Lemma prod_equivI {A B : cofeT} (x y : A * B) : x ≡ y ⊣⊢ x.1 ≡ y.1 ∧ x.2 ≡ y.2.
 Proof. by unseal. Qed.
-Lemma prod_validI {A B : cmraT} (x : A * B) :
-  (✓ x) ⊣⊢ (✓ x.1 ∧ ✓ x.2).
+Lemma prod_validI {A B : cmraT} (x : A * B) : ✓ x ⊣⊢ ✓ x.1 ∧ ✓ x.2.
 Proof. by unseal. Qed.
 
 (* Later *)
 Lemma later_equivI {A : cofeT} (x y : later A) :
-  (x ≡ y) ⊣⊢ (▷ (later_car x ≡ later_car y)).
+  x ≡ y ⊣⊢ ▷ (later_car x ≡ later_car y).
 Proof. by unseal. Qed.
 
 (* Discrete *)
-Lemma discrete_valid {A : cmraT} `{!CMRADiscrete A} (a : A) : (✓ a) ⊣⊢ ■ ✓ a.
+Lemma discrete_valid {A : cmraT} `{!CMRADiscrete A} (a : A) : ✓ a ⊣⊢ ■ ✓ a.
 Proof. unseal; split=> n x _. by rewrite /= -cmra_discrete_valid_iff. Qed.
-Lemma timeless_eq {A : cofeT} (a b : A) :
-  Timeless a → (a ≡ b) ⊣⊢ ■ (a ≡ b).
+Lemma timeless_eq {A : cofeT} (a b : A) : Timeless a → a ≡ b ⊣⊢ ■ (a ≡ b).
 Proof.
   unseal=> ?. apply (anti_symm (⊢)); split=> n x ?; by apply (timeless_iff n).
 Qed.
 
 (* Option *)
 Lemma option_equivI {A : cofeT} (mx my : option A) :
-  (mx ≡ my) ⊣⊢ (match mx, my with
-                | Some x, Some y => x ≡ y | None, None => True | _, _ => False
-                end : uPred M).
+  mx ≡ my ⊣⊢ match mx, my with
+             | Some x, Some y => x ≡ y | None, None => True | _, _ => False
+             end.
 Proof.
   uPred.unseal. do 2 split. by destruct 1. by destruct mx, my; try constructor.
 Qed.
 Lemma option_validI {A : cmraT} (mx : option A) :
-  (✓ mx) ⊣⊢ (match mx with Some x => ✓ x | None => True end : uPred M).
+  ✓ mx ⊣⊢ match mx with Some x => ✓ x | None => True end.
 Proof. uPred.unseal. by destruct mx. Qed.
 
 (* Timeless *)
@@ -1199,17 +1195,17 @@ Lemma always_always P `{!PersistentP P} : □ P ⊣⊢ P.
 Proof. apply (anti_symm (⊢)); auto using always_elim. Qed.
 Lemma always_if_always p P `{!PersistentP P} : □?p P ⊣⊢ P.
 Proof. destruct p; simpl; auto using always_always. Qed.
-Lemma always_intro P Q `{!PersistentP P} : P ⊢ Q → P ⊢ □ Q.
+Lemma always_intro P Q `{!PersistentP P} : (P ⊢ Q) → P ⊢ □ Q.
 Proof. rewrite -(always_always P); apply always_intro'. Qed.
-Lemma always_and_sep_l P Q `{!PersistentP P} : (P ∧ Q) ⊣⊢ (P ★ Q).
+Lemma always_and_sep_l P Q `{!PersistentP P} : P ∧ Q ⊣⊢ P ★ Q.
 Proof. by rewrite -(always_always P) always_and_sep_l'. Qed.
-Lemma always_and_sep_r P Q `{!PersistentP Q} : (P ∧ Q) ⊣⊢ (P ★ Q).
+Lemma always_and_sep_r P Q `{!PersistentP Q} : P ∧ Q ⊣⊢ P ★ Q.
 Proof. by rewrite -(always_always Q) always_and_sep_r'. Qed.
-Lemma always_sep_dup P `{!PersistentP P} : P ⊣⊢ (P ★ P).
+Lemma always_sep_dup P `{!PersistentP P} : P ⊣⊢ P ★ P.
 Proof. by rewrite -(always_always P) -always_sep_dup'. Qed.
-Lemma always_entails_l P Q `{!PersistentP Q} : (P ⊢ Q) → P ⊢ (Q ★ P).
+Lemma always_entails_l P Q `{!PersistentP Q} : (P ⊢ Q) → P ⊢ Q ★ P.
 Proof. by rewrite -(always_always Q); apply always_entails_l'. Qed.
-Lemma always_entails_r P Q `{!PersistentP Q} : (P ⊢ Q) → P ⊢ (P ★ Q).
+Lemma always_entails_r P Q `{!PersistentP Q} : (P ⊢ Q) → P ⊢ P ★ Q.
 Proof. by rewrite -(always_always Q); apply always_entails_r'. Qed.
 End uPred_logic.
 
diff --git a/algebra/upred_big_op.v b/algebra/upred_big_op.v
index d25e6fd85b92c5e9c19794c748311017c8f12c65..100ba776d5cae9daa499c6d181bac9ddafd7fae5 100644
--- a/algebra/upred_big_op.v
+++ b/algebra/upred_big_op.v
@@ -83,9 +83,9 @@ Proof.
   - etrans; eauto.
 Qed.
 
-Lemma big_and_app Ps Qs : [∧] (Ps ++ Qs) ⊣⊢ ([∧] Ps ∧ [∧] Qs).
+Lemma big_and_app Ps Qs : [∧] (Ps ++ Qs) ⊣⊢ [∧] Ps ∧ [∧] Qs.
 Proof. induction Ps as [|?? IH]; by rewrite /= ?left_id -?assoc ?IH. Qed.
-Lemma big_sep_app Ps Qs : [★] (Ps ++ Qs) ⊣⊢ ([★] Ps ★ [★] Qs).
+Lemma big_sep_app Ps Qs : [★] (Ps ++ Qs) ⊣⊢ [★] Ps ★ [★] Qs.
 Proof. by induction Ps as [|?? IH]; rewrite /= ?left_id -?assoc ?IH. Qed.
 
 Lemma big_and_contains Ps Qs : Qs `contains` Ps → [∧] Ps ⊢ [∧] Qs.
@@ -113,7 +113,7 @@ Section gmap.
 
   Lemma big_sepM_mono Φ Ψ m1 m2 :
     m2 ⊆ m1 → (∀ k x, m2 !! k = Some x → Φ k x ⊢ Ψ k x) →
-    ([★ map] k ↦ x ∈ m1, Φ k x) ⊢ ([★ map] k ↦ x ∈ m2, Ψ k x).
+    ([★ map] k ↦ x ∈ m1, Φ k x) ⊢ [★ map] k ↦ x ∈ m2, Ψ k x.
   Proof.
     intros HX HΦ. trans ([★ map] k↦x ∈ m2, Φ k x)%I.
     - by apply big_sep_contains, fmap_contains, map_to_list_contains.
@@ -152,12 +152,12 @@ Section gmap.
 
   Lemma big_sepM_insert Φ m i x :
     m !! i = None →
-    ([★ map] k↦y ∈ <[i:=x]> m, Φ k y) ⊣⊢ (Φ i x ★ [★ map] k↦y ∈ m, Φ k y).
+    ([★ map] k↦y ∈ <[i:=x]> m, Φ k y) ⊣⊢ Φ i x ★ [★ map] k↦y ∈ m, Φ k y.
   Proof. intros ?; by rewrite /uPred_big_sepM map_to_list_insert. Qed.
 
   Lemma big_sepM_delete Φ m i x :
     m !! i = Some x →
-    ([★ map] k↦y ∈ m, Φ k y) ⊣⊢ (Φ i x ★ [★ map] k↦y ∈ delete i m, Φ k y).
+    ([★ map] k↦y ∈ m, Φ k y) ⊣⊢ Φ i x ★ [★ map] k↦y ∈ delete i m, Φ k y.
   Proof.
     intros. rewrite -big_sepM_insert ?lookup_delete //.
     by rewrite insert_delete insert_id.
@@ -204,7 +204,7 @@ Section gmap.
 
   Lemma big_sepM_sepM Φ Ψ m :
        ([★ map] k↦x ∈ m, Φ k x ★ Ψ k x)
-    ⊣⊢ (([★ map] k↦x ∈ m, Φ k x) ★ ([★ map] k↦x ∈ m, Ψ k x)).
+    ⊣⊢ ([★ map] k↦x ∈ m, Φ k x) ★ ([★ map] k↦x ∈ m, Ψ k x).
   Proof.
     rewrite /uPred_big_sepM.
     induction (map_to_list m) as [|[i x] l IH]; csimpl; rewrite ?right_id //.
@@ -212,7 +212,7 @@ Section gmap.
   Qed.
 
   Lemma big_sepM_later Φ m :
-    (▷ [★ map] k↦x ∈ m, Φ k x) ⊣⊢ ([★ map] k↦x ∈ m, ▷ Φ k x).
+    ▷ ([★ map] k↦x ∈ m, Φ k x) ⊣⊢ ([★ map] k↦x ∈ m, ▷ Φ k x).
   Proof.
     rewrite /uPred_big_sepM.
     induction (map_to_list m) as [|[i x] l IH]; csimpl; rewrite ?later_True //.
@@ -228,7 +228,7 @@ Section gmap.
   Qed.
 
   Lemma big_sepM_always_if p Φ m :
-    (□?p [★ map] k↦x ∈ m, Φ k x) ⊣⊢ ([★ map] k↦x ∈ m, □?p Φ k x).
+    □?p ([★ map] k↦x ∈ m, Φ k x) ⊣⊢ ([★ map] k↦x ∈ m, □?p Φ k x).
   Proof. destruct p; simpl; auto using big_sepM_always. Qed.
 
   Lemma big_sepM_forall Φ m :
@@ -249,7 +249,7 @@ Section gmap.
   Qed.
 
   Lemma big_sepM_impl Φ Ψ m :
-      (□ (∀ k x, m !! k = Some x → Φ k x → Ψ k x) ∧ [★ map] k↦x ∈ m, Φ k x)
+    □ (∀ k x, m !! k = Some x → Φ k x → Ψ k x) ∧ ([★ map] k↦x ∈ m, Φ k x)
     ⊢ [★ map] k↦x ∈ m, Ψ k x.
   Proof.
     rewrite always_and_sep_l. do 2 setoid_rewrite always_forall.
@@ -267,7 +267,7 @@ Section gset.
 
   Lemma big_sepS_mono Φ Ψ X Y :
     Y ⊆ X → (∀ x, x ∈ Y → Φ x ⊢ Ψ x) →
-    ([★ set] x ∈ X, Φ x) ⊢ ([★ set] x ∈ Y, Ψ x).
+    ([★ set] x ∈ X, Φ x) ⊢ [★ set] x ∈ Y, Ψ x.
   Proof.
     intros HX HΦ. trans ([★ set] x ∈ Y, Φ x)%I.
     - by apply big_sep_contains, fmap_contains, elements_contains.
@@ -315,7 +315,7 @@ Section gset.
   Proof. apply (big_sepS_fn_insert (λ y, id)). Qed.
 
   Lemma big_sepS_delete Φ X x :
-    x ∈ X → ([★ set] y ∈ X, Φ y) ⊣⊢ (Φ x ★ [★ set] y ∈ X ∖ {[ x ]}, Φ y).
+    x ∈ X → ([★ set] y ∈ X, Φ y) ⊣⊢ Φ x ★ [★ set] y ∈ X ∖ {[ x ]}, Φ y.
   Proof.
     intros. rewrite -big_sepS_insert; last set_solver.
     by rewrite -union_difference_L; last set_solver.
@@ -328,21 +328,21 @@ Section gset.
   Proof. intros. by rewrite /uPred_big_sepS elements_singleton /= right_id. Qed.
 
   Lemma big_sepS_sepS Φ Ψ X :
-    ([★ set] y ∈ X, Φ y ★ Ψ y) ⊣⊢ (([★ set] y ∈ X, Φ y) ★ [★ set] y ∈ X, Ψ y).
+    ([★ set] y ∈ X, Φ y ★ Ψ y) ⊣⊢ ([★ set] y ∈ X, Φ y) ★ ([★ set] y ∈ X, Ψ y).
   Proof.
     rewrite /uPred_big_sepS.
     induction (elements X) as [|x l IH]; csimpl; first by rewrite ?right_id.
     by rewrite IH -!assoc (assoc _ (Ψ _)) [(Ψ _ ★ _)%I]comm -!assoc.
   Qed.
 
-  Lemma big_sepS_later Φ X : (▷ [★ set] y ∈ X, Φ y) ⊣⊢ ([★ set] y ∈ X, ▷ Φ y).
+  Lemma big_sepS_later Φ X : ▷ ([★ set] y ∈ X, Φ y) ⊣⊢ ([★ set] y ∈ X, ▷ Φ y).
   Proof.
     rewrite /uPred_big_sepS.
     induction (elements X) as [|x l IH]; csimpl; first by rewrite ?later_True.
     by rewrite later_sep IH.
   Qed.
 
-  Lemma big_sepS_always Φ X : (□ [★ set] y ∈ X, Φ y) ⊣⊢ ([★ set] y ∈ X, □ Φ y).
+  Lemma big_sepS_always Φ X : □ ([★ set] y ∈ X, Φ y) ⊣⊢ ([★ set] y ∈ X, □ Φ y).
   Proof.
     rewrite /uPred_big_sepS.
     induction (elements X) as [|x l IH]; csimpl; first by rewrite ?always_const.
@@ -350,7 +350,7 @@ Section gset.
   Qed.
 
   Lemma big_sepS_always_if q Φ X :
-    (□?q [★ set] y ∈ X, Φ y) ⊣⊢ ([★ set] y ∈ X, □?q Φ y).
+    □?q ([★ set] y ∈ X, Φ y) ⊣⊢ ([★ set] y ∈ X, □?q Φ y).
   Proof. destruct q; simpl; auto using big_sepS_always. Qed.
 
   Lemma big_sepS_forall Φ X :
@@ -369,7 +369,7 @@ Section gset.
   Qed.
 
   Lemma big_sepS_impl Φ Ψ X :
-      (□ (∀ x, ■ (x ∈ X) → Φ x → Ψ x) ∧ [★ set] x ∈ X, Φ x) ⊢ [★ set] x ∈ X, Ψ x.
+      □ (∀ x, ■ (x ∈ X) → Φ x → Ψ x) ∧ ([★ set] x ∈ X, Φ x) ⊢ [★ set] x ∈ X, Ψ x.
   Proof.
     rewrite always_and_sep_l always_forall.
     setoid_rewrite always_impl; setoid_rewrite always_const.
diff --git a/algebra/upred_tactics.v b/algebra/upred_tactics.v
index d92c6fa88b13497c3095761e50fe624388536e56..34ba9a25e550e023efe44ac283e39d0b200c3eca 100644
--- a/algebra/upred_tactics.v
+++ b/algebra/upred_tactics.v
@@ -86,7 +86,7 @@ Module uPred_reflection. Section uPred_reflection.
   Qed.
   Lemma cancel_entails Σ e1 e2 e1' e2' ns :
     cancel ns e1 = Some e1' → cancel ns e2 = Some e2' →
-    eval Σ e1' ⊢ eval Σ e2' → eval Σ e1 ⊢ eval Σ e2.
+    (eval Σ e1' ⊢ eval Σ e2') → eval Σ e1 ⊢ eval Σ e2.
   Proof.
     intros ??. rewrite !eval_flatten.
     rewrite (flatten_cancel e1 e1' ns) // (flatten_cancel e2 e2' ns) //; csimpl.
diff --git a/heap_lang/lib/barrier/proof.v b/heap_lang/lib/barrier/proof.v
index e0babf96c7689e467e33113cf60b3b5e5cbaf9fb..bca2c4d0f1ff9834dd60032012cfef36a25b2065 100644
--- a/heap_lang/lib/barrier/proof.v
+++ b/heap_lang/lib/barrier/proof.v
@@ -77,8 +77,8 @@ Proof. solve_proper. Qed.
 (** Helper lemmas *)
 Lemma ress_split i i1 i2 Q R1 R2 P I :
   i ∈ I → i1 ∉ I → i2 ∉ I → i1 ≠ i2 →
-  (saved_prop_own i Q ★ saved_prop_own i1 R1 ★ saved_prop_own i2 R2 ★
-    (Q -★ R1 ★ R2) ★ ress P I)
+  saved_prop_own i Q ★ saved_prop_own i1 R1 ★ saved_prop_own i2 R2 ★
+    (Q -★ R1 ★ R2) ★ ress P I
   ⊢ ress P ({[i1;i2]} ∪ I ∖ {[i]}).
 Proof.
   iIntros {????} "(#HQ&#H1&#H2&HQR&H)"; iDestruct "H" as {Ψ} "[HPΨ HΨ]".
@@ -97,7 +97,7 @@ Qed.
 (** Actual proofs *)
 Lemma newbarrier_spec (P : iProp) (Φ : val → iProp) :
   heapN ⊥ N →
-  (heap_ctx heapN ★ ∀ l, recv l P ★ send l P -★ Φ #l)
+  heap_ctx heapN ★ (∀ l, recv l P ★ send l P -★ Φ #l)
   ⊢ WP newbarrier #() {{ Φ }}.
 Proof.
   iIntros {HN} "[#? HΦ]".
@@ -124,7 +124,7 @@ Proof.
 Qed.
 
 Lemma signal_spec l P (Φ : val → iProp) :
-  (send l P ★ P ★ Φ #()) ⊢ WP signal #l {{ Φ }}.
+  send l P ★ P ★ Φ #() ⊢ WP signal #l {{ Φ }}.
 Proof.
   rewrite /signal /send /barrier_ctx.
   iIntros "(Hs&HP&HΦ)"; iDestruct "Hs" as {γ} "[#(%&Hh&Hsts) Hγ]". wp_let.
@@ -139,7 +139,7 @@ Proof.
 Qed.
 
 Lemma wait_spec l P (Φ : val → iProp) :
-  (recv l P ★ (P -★ Φ #())) ⊢ WP wait #l {{ Φ }}.
+  recv l P ★ (P -★ Φ #()) ⊢ WP wait #l {{ Φ }}.
 Proof.
   rename P into R; rewrite /recv /barrier_ctx.
   iIntros "[Hr HΦ]"; iDestruct "Hr" as {γ P Q i} "(#(%&Hh&Hsts)&Hγ&#HQ&HQR)".
@@ -200,7 +200,7 @@ Proof.
       by iIntros "> ?".
 Qed.
 
-Lemma recv_weaken l P1 P2 : (P1 -★ P2) ⊢ (recv l P1 -★ recv l P2).
+Lemma recv_weaken l P1 P2 : (P1 -★ P2) ⊢ recv l P1 -★ recv l P2.
 Proof.
   rewrite /recv.
   iIntros "HP HP1"; iDestruct "HP1" as {γ P Q i} "(#Hctx&Hγ&Hi&HP1)".
@@ -208,7 +208,7 @@ Proof.
   iIntros "> HQ". by iApply "HP"; iApply "HP1".
 Qed.
 
-Lemma recv_mono l P1 P2 : P1 ⊢ P2 → recv l P1 ⊢ recv l P2.
+Lemma recv_mono l P1 P2 : (P1 ⊢ P2) → recv l P1 ⊢ recv l P2.
 Proof.
   intros HP%entails_wand. apply wand_entails. rewrite HP. apply recv_weaken.
 Qed.
diff --git a/heap_lang/lib/barrier/specification.v b/heap_lang/lib/barrier/specification.v
index f0b23398328c1cf99ee86b4180a919e9facba855..1513ddc7dfaaf3b9660fd523ce9e8dd2ec1b5147 100644
--- a/heap_lang/lib/barrier/specification.v
+++ b/heap_lang/lib/barrier/specification.v
@@ -17,7 +17,7 @@ Lemma barrier_spec (heapN N : namespace) :
     (∀ l P, {{ send l P ★ P }} signal #l {{ _, True }}) ∧
     (∀ l P, {{ recv l P }} wait #l {{ _, P }}) ∧
     (∀ l P Q, recv l (P ★ Q) ={N}=> recv l P ★ recv l Q) ∧
-    (∀ l P Q, (P -★ Q) ⊢ (recv l P -★ recv l Q)).
+    (∀ l P Q, (P -★ Q) ⊢ recv l P -★ recv l Q).
 Proof.
   intros HN.
   exists (λ l, CofeMor (recv heapN N l)), (λ l, CofeMor (send heapN N l)).
diff --git a/heap_lang/lib/lock.v b/heap_lang/lib/lock.v
index 8b1b522ceca6dd4516ceab6f719f74129609e4f5..1d4300f9477c767f2085fd22d5272832967a3b67 100644
--- a/heap_lang/lib/lock.v
+++ b/heap_lang/lib/lock.v
@@ -51,8 +51,7 @@ Qed.
 
 Lemma newlock_spec N (R : iProp) Φ :
   heapN ⊥ N →
-  (heap_ctx heapN ★ R ★ (∀ l, is_lock l R -★ Φ #l))
-  ⊢ WP newlock #() {{ Φ }}.
+  heap_ctx heapN ★ R ★ (∀ l, is_lock l R -★ Φ #l) ⊢ WP newlock #() {{ Φ }}.
 Proof.
   iIntros {?} "(#Hh & HR & HΦ)". rewrite /newlock.
   wp_seq. iApply wp_pvs. wp_alloc l as "Hl".
@@ -63,7 +62,7 @@ Proof.
 Qed.
 
 Lemma acquire_spec l R (Φ : val → iProp) :
-  (is_lock l R ★ (locked l R -★ R -★ Φ #())) ⊢ WP acquire #l {{ Φ }}.
+  is_lock l R ★ (locked l R -★ R -★ Φ #()) ⊢ WP acquire #l {{ Φ }}.
 Proof.
   iIntros "[Hl HΦ]". iDestruct "Hl" as {N γ} "(%&#?&#?)".
   iLöb as "IH". wp_rec. wp_focus (CAS _ _ _)%E.
@@ -77,7 +76,7 @@ Proof.
 Qed.
 
 Lemma release_spec R l (Φ : val → iProp) :
-  (locked l R ★ R ★ Φ #()) ⊢ WP release #l {{ Φ }}.
+  locked l R ★ R ★ Φ #() ⊢ WP release #l {{ Φ }}.
 Proof.
   iIntros "(Hl&HR&HΦ)"; iDestruct "Hl" as {N γ} "(% & #? & #? & Hγ)".
   rewrite /release. wp_let. iInv N as {b} "[Hl _]".
diff --git a/heap_lang/lib/spawn.v b/heap_lang/lib/spawn.v
index b2f5f24beb19b4def7281d5370c93c726446a98c..685d451728d98178e3c374a9e39258896dd80567 100644
--- a/heap_lang/lib/spawn.v
+++ b/heap_lang/lib/spawn.v
@@ -54,7 +54,7 @@ Proof. solve_proper. Qed.
 Lemma spawn_spec (Ψ : val → iProp) e (f : val) (Φ : val → iProp) :
   to_val e = Some f →
   heapN ⊥ N →
-  (heap_ctx heapN ★ WP f #() {{ Ψ }} ★ ∀ l, join_handle l Ψ -★ Φ #l)
+  heap_ctx heapN ★ WP f #() {{ Ψ }} ★ (∀ l, join_handle l Ψ -★ Φ #l)
   ⊢ WP spawn e {{ Φ }}.
 Proof.
   iIntros {<-%of_to_val ?} "(#Hh&Hf&HΦ)". rewrite /spawn.
@@ -72,7 +72,7 @@ Proof.
 Qed.
 
 Lemma join_spec (Ψ : val → iProp) l (Φ : val → iProp) :
-  (join_handle l Ψ ★ ∀ v, Ψ v -★ Φ v) ⊢ WP join #l {{ Φ }}.
+  join_handle l Ψ ★ (∀ v, Ψ v -★ Φ v) ⊢ WP join #l {{ Φ }}.
 Proof.
   rewrite /join_handle; iIntros "[[% H] Hv]"; iDestruct "H" as {γ} "(#?&Hγ&#?)".
   iLöb as "IH". wp_rec. wp_focus (! _)%E. iInv N as {v} "[Hl Hinv]".
diff --git a/heap_lang/proofmode.v b/heap_lang/proofmode.v
index 9cf51479499ca311151c300bef3cb8d7594426a3..bd01b72a48afe156209c2d1dd0d4c1dc19ed08de 100644
--- a/heap_lang/proofmode.v
+++ b/heap_lang/proofmode.v
@@ -18,11 +18,11 @@ Proof. by rewrite /SepDestruct heap_mapsto_op_split. Qed.
 
 Lemma tac_wp_alloc Δ Δ' N E j e v Φ :
   to_val e = Some v → 
-  Δ ⊢ heap_ctx N → nclose N ⊆ E →
+  (Δ ⊢ heap_ctx N) → nclose N ⊆ E →
   StripLaterEnvs Δ Δ' →
   (∀ l, ∃ Δ'',
     envs_app false (Esnoc Enil j (l ↦ v)) Δ' = Some Δ'' ∧
-    Δ'' ⊢ Φ (LitV (LitLoc l))) →
+    (Δ'' ⊢ Φ (LitV (LitLoc l)))) →
   Δ ⊢ WP Alloc e @ E {{ Φ }}.
 Proof.
   intros ???? HΔ. rewrite -wp_alloc // -always_and_sep_l.
@@ -33,10 +33,10 @@ Proof.
 Qed.
 
 Lemma tac_wp_load Δ Δ' N E i l q v Φ :
-  Δ ⊢ heap_ctx N → nclose N ⊆ E →
+  (Δ ⊢ heap_ctx N) → nclose N ⊆ E →
   StripLaterEnvs Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦{q} v)%I →
-  Δ' ⊢ Φ v →
+  (Δ' ⊢ Φ v) →
   Δ ⊢ WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
 Proof.
   intros. rewrite -wp_load // -always_and_sep_l. apply and_intro; first done.
@@ -46,11 +46,11 @@ Qed.
 
 Lemma tac_wp_store Δ Δ' Δ'' N E i l v e v' Φ :
   to_val e = Some v' →
-  Δ ⊢ heap_ctx N → nclose N ⊆ E →
+  (Δ ⊢ heap_ctx N) → nclose N ⊆ E →
   StripLaterEnvs Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦ v)%I →
   envs_simple_replace i false (Esnoc Enil i (l ↦ v')) Δ' = Some Δ'' →
-  Δ'' ⊢ Φ (LitV LitUnit) → Δ ⊢ WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
+  (Δ'' ⊢ Φ (LitV LitUnit)) → Δ ⊢ WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
 Proof.
   intros. rewrite -wp_store // -always_and_sep_l. apply and_intro; first done.
   rewrite strip_later_env_sound -later_sep envs_simple_replace_sound //; simpl.
@@ -59,10 +59,10 @@ Qed.
 
 Lemma tac_wp_cas_fail Δ Δ' N E i l q v e1 v1 e2 v2 Φ :
   to_val e1 = Some v1 → to_val e2 = Some v2 →
-  Δ ⊢ heap_ctx N → nclose N ⊆ E →
+  (Δ ⊢ heap_ctx N) → nclose N ⊆ E →
   StripLaterEnvs Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦{q} v)%I → v ≠ v1 →
-  Δ' ⊢ Φ (LitV (LitBool false)) →
+  (Δ' ⊢ Φ (LitV (LitBool false))) →
   Δ ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
 Proof.
   intros. rewrite -wp_cas_fail // -always_and_sep_l. apply and_intro; first done.
@@ -72,11 +72,11 @@ Qed.
 
 Lemma tac_wp_cas_suc Δ Δ' Δ'' N E i l v e1 v1 e2 v2 Φ :
   to_val e1 = Some v1 → to_val e2 = Some v2 →
-  Δ ⊢ heap_ctx N → nclose N ⊆ E →
+  (Δ ⊢ heap_ctx N) → nclose N ⊆ E →
   StripLaterEnvs Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦ v)%I → v = v1 →
   envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ' = Some Δ'' →
-  Δ'' ⊢ Φ (LitV (LitBool true)) → Δ ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
+  (Δ'' ⊢ Φ (LitV (LitBool true))) → Δ ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
 Proof.
   intros; subst.
   rewrite -wp_cas_suc // -always_and_sep_l. apply and_intro; first done.
diff --git a/program_logic/adequacy.v b/program_logic/adequacy.v
index f5eab2f097c041d58c0345a7bc959454b6b7cfbc..1219034a305f7387b0ae2580c5f12f229c75e645 100644
--- a/program_logic/adequacy.v
+++ b/program_logic/adequacy.v
@@ -56,7 +56,7 @@ Proof.
     by rewrite -Permutation_middle /= big_op_app.
 Qed.
 Lemma wp_adequacy_steps P Φ k n e1 t2 σ1 σ2 r1 :
-  P ⊢ WP e1 {{ Φ }} →
+  (P ⊢ WP e1 {{ Φ }}) →
   nsteps step k ([e1],σ1) (t2,σ2) →
   1 < n → wsat (k + n) ⊤ σ1 r1 →
   P (k + n) r1 →
@@ -70,7 +70,7 @@ Qed.
 
 Lemma wp_adequacy_own Φ e1 t2 σ1 m σ2 :
   ✓ m →
-  (ownP σ1 ★ ownG m) ⊢ WP e1 {{ Φ }} →
+  (ownP σ1 ★ ownG m ⊢ WP e1 {{ Φ }}) →
   rtc step ([e1],σ1) (t2,σ2) →
   ∃ rs2 Φs', wptp 2 t2 (Φ :: Φs') rs2 ∧ wsat 2 ⊤ σ2 (big_op rs2).
 Proof.
@@ -85,7 +85,7 @@ Qed.
 
 Theorem wp_adequacy_result E φ e v t2 σ1 m σ2 :
   ✓ m →
-  (ownP σ1 ★ ownG m) ⊢ WP e @ E {{ v', ■ φ v' }} →
+  (ownP σ1 ★ ownG m ⊢ WP e @ E {{ v', ■ φ v' }}) →
   rtc step ([e], σ1) (of_val v :: t2, σ2) →
   φ v.
 Proof.
@@ -111,7 +111,7 @@ Qed.
 
 Lemma wp_adequacy_reducible E Φ e1 e2 t2 σ1 m σ2 :
   ✓ m →
-  (ownP σ1 ★ ownG m) ⊢ WP e1 @ E {{ Φ }} →
+  (ownP σ1 ★ ownG m ⊢ WP e1 @ E {{ Φ }}) →
   rtc step ([e1], σ1) (t2, σ2) →
   e2 ∈ t2 → (is_Some (to_val e2) ∨ reducible e2 σ2).
 Proof.
@@ -129,7 +129,7 @@ Qed.
 (* Connect this up to the threadpool-semantics. *)
 Theorem wp_adequacy_safe E Φ e1 t2 σ1 m σ2 :
   ✓ m →
-  (ownP σ1 ★ ownG m) ⊢ WP e1 @ E {{ Φ }} →
+  (ownP σ1 ★ ownG m ⊢ WP e1 @ E {{ Φ }}) →
   rtc step ([e1], σ1) (t2, σ2) →
   Forall (λ e, is_Some (to_val e)) t2 ∨ ∃ t3 σ3, step (t2, σ2) (t3, σ3).
 Proof.
diff --git a/program_logic/auth.v b/program_logic/auth.v
index 0254e3c11ff1a852a04ff0fdcae8fac49d9c8ffa..29bf57dc3b56c5745825cb8e6d8ea6a688568bd3 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -75,7 +75,8 @@ Section auth.
     ✓ a → nclose N ⊆ E →
     ▷ φ a ={E}=> ∃ γ, auth_ctx γ N φ ∧ auth_own γ a.
   Proof.
-    iIntros {??} "Hφ". iPvs (auth_alloc_strong N E a ∅ with "Hφ") as {γ} "[_ ?]"; [done..|].
+    iIntros {??} "Hφ".
+    iPvs (auth_alloc_strong N E a ∅ with "Hφ") as {γ} "[_ ?]"; [done..|].
     by iExists γ.
   Qed.
 
@@ -86,7 +87,7 @@ Section auth.
 
   Lemma auth_fsa E N (Ψ : V → iPropG Λ Σ) γ a :
     fsaV → nclose N ⊆ E →
-    (auth_ctx γ N φ ★ ▷ auth_own γ a ★ ∀ a',
+    auth_ctx γ N φ ★ ▷ auth_own γ a ★ (∀ a',
       ■ ✓ (a ⋅ a') ★ ▷ φ (a ⋅ a') -★
       fsa (E ∖ nclose N) (λ x, ∃ L Lv (Hup : LocalUpdate Lv L),
         ■ (Lv a ∧ ✓ (L a ⋅ a')) ★ ▷ φ (L a ⋅ a') ★
@@ -111,11 +112,11 @@ Section auth.
 
   Lemma auth_fsa' L `{!LocalUpdate Lv L} E N (Ψ : V → iPropG Λ Σ) γ a :
     fsaV → nclose N ⊆ E →
-    (auth_ctx γ N φ ★ ▷ auth_own γ a ★ (∀ a',
+    auth_ctx γ N φ ★ ▷ auth_own γ a ★ (∀ a',
       ■ ✓ (a ⋅ a') ★ ▷ φ (a ⋅ a') -★
       fsa (E ∖ nclose N) (λ x,
         ■ (Lv a ∧ ✓ (L a ⋅ a')) ★ ▷ φ (L a ⋅ a') ★
-        (auth_own γ (L a) -★ Ψ x))))
+        (auth_own γ (L a) -★ Ψ x)))
     ⊢ fsa E Ψ.
   Proof.
     iIntros {??} "(#Ha & Hγf & HΨ)"; iApply (auth_fsa E N Ψ γ a); auto.
diff --git a/program_logic/boxes.v b/program_logic/boxes.v
index cd6d14f70a83a29c83e29b99ad4ef2e367b5225a..6cabfb8524238b80c5cd438690498219e1310bb3 100644
--- a/program_logic/boxes.v
+++ b/program_logic/boxes.v
@@ -61,7 +61,7 @@ Instance box_own_auth_timeless γ
 Proof. apply own_timeless, pair_timeless; apply _. Qed.
 
 Lemma box_own_auth_agree γ b1 b2 :
-  (box_own_auth γ (● Excl' b1) ★ box_own_auth γ (◯ Excl' b2)) ⊢ (b1 = b2).
+  box_own_auth γ (● Excl' b1) ★ box_own_auth γ (◯ Excl' b2) ⊢ b1 = b2.
 Proof.
   rewrite /box_own_prop -own_op own_valid prod_validI /= and_elim_l.
   iIntros "Hb".
diff --git a/program_logic/ectx_lifting.v b/program_logic/ectx_lifting.v
index 07a5f07f6ec4c180b72723946e05c12bd661b36d..fd0df37bf038959a9b6477045989508107f797e3 100644
--- a/program_logic/ectx_lifting.v
+++ b/program_logic/ectx_lifting.v
@@ -38,9 +38,8 @@ Lemma wp_lift_atomic_head_step {E Φ} e1
     (φ : expr → state → option expr → Prop) σ1 :
   atomic e1 →
   head_reducible e1 σ1 →
-  (∀ e2 σ2 ef,
-    head_step e1 σ1 e2 σ2 ef → φ e2 σ2 ef) →
-  (▷ ownP σ1 ★ ▷ ∀ v2 σ2 ef, ■ φ (of_val v2) σ2 ef ∧ ownP σ2 -★ Φ v2 ★ wp_fork ef)
+  (∀ e2 σ2 ef, head_step e1 σ1 e2 σ2 ef → φ e2 σ2 ef) →
+  ▷ ownP σ1 ★ ▷ (∀ v2 σ2 ef, ■ φ (of_val v2) σ2 ef ∧ ownP σ2 -★ Φ v2 ★ wp_fork ef)
   ⊢ WP e1 @ E {{ Φ }}.
 Proof. eauto using wp_lift_atomic_step. Qed.
 
@@ -49,7 +48,7 @@ Lemma wp_lift_atomic_det_head_step {E Φ e1} σ1 v2 σ2 ef :
   head_reducible e1 σ1 →
   (∀ e2' σ2' ef', head_step e1 σ1 e2' σ2' ef' →
     σ2 = σ2' ∧ to_val e2' = Some v2 ∧ ef = ef') →
-  (▷ ownP σ1 ★ ▷ (ownP σ2 -★ Φ v2 ★ wp_fork ef)) ⊢ WP e1 @ E {{ Φ }}.
+  ▷ ownP σ1 ★ ▷ (ownP σ2 -★ Φ v2 ★ wp_fork ef) ⊢ WP e1 @ E {{ Φ }}.
 Proof. eauto using wp_lift_atomic_det_step. Qed.
 
 Lemma wp_lift_pure_det_head_step {E Φ} e1 e2 ef :
diff --git a/program_logic/ghost_ownership.v b/program_logic/ghost_ownership.v
index b3e98ab0dbdcef4bf7c7ac7e2c757faebc4295fa..29605843d29e76fb104c47f60ea726d3219f23df 100644
--- a/program_logic/ghost_ownership.v
+++ b/program_logic/ghost_ownership.v
@@ -19,7 +19,7 @@ Global Instance own_ne γ n : Proper (dist n ==> dist n) (own γ).
 Proof. solve_proper. Qed.
 Global Instance own_proper γ : Proper ((≡) ==> (⊣⊢)) (own γ) := ne_proper _.
 
-Lemma own_op γ a1 a2 : own γ (a1 ⋅ a2) ⊣⊢ (own γ a1 ★ own γ a2).
+Lemma own_op γ a1 a2 : own γ (a1 ⋅ a2) ⊣⊢ own γ a1 ★ own γ a2.
 Proof. by rewrite /own -ownG_op to_globalF_op. Qed.
 Global Instance own_mono γ : Proper (flip (≼) ==> (⊢)) (own γ).
 Proof. move=>a b [c ->]. rewrite own_op. eauto with I. Qed.
@@ -31,9 +31,9 @@ Proof.
   (* implicit arguments differ a bit *)
   by trans (✓ cmra_transport inG_prf a : iPropG Λ Σ)%I; last destruct inG_prf.
 Qed.
-Lemma own_valid_r γ a : own γ a ⊢ (own γ a ★ ✓ a).
+Lemma own_valid_r γ a : own γ a ⊢ own γ a ★ ✓ a.
 Proof. apply: uPred.always_entails_r. apply own_valid. Qed.
-Lemma own_valid_l γ a : own γ a ⊢ (✓ a ★ own γ a).
+Lemma own_valid_l γ a : own γ a ⊢ ✓ a ★ own γ a.
 Proof. by rewrite comm -own_valid_r. Qed.
 Global Instance own_timeless γ a : Timeless a → TimelessP (own γ a).
 Proof. rewrite /own; apply _. Qed.
diff --git a/program_logic/hoare.v b/program_logic/hoare.v
index 8745e5e491276fa6e2d224d85e57911d4c8a1918..ef46d9880e9e884c5c9b12c95df6108db619cb84 100644
--- a/program_logic/hoare.v
+++ b/program_logic/hoare.v
@@ -46,7 +46,7 @@ Global Instance ht_proper E :
   Proper ((≡) ==> eq ==> pointwise_relation _ (≡) ==> (≡)) (@ht Λ Σ E).
 Proof. solve_proper. Qed.
 Lemma ht_mono E P P' Φ Φ' e :
-  P ⊢ P' → (∀ v, Φ' v ⊢ Φ v) → {{ P' }} e @ E {{ Φ' }} ⊢ {{ P }} e @ E {{ Φ }}.
+  (P ⊢ P') → (∀ v, Φ' v ⊢ Φ v) → {{ P' }} e @ E {{ Φ' }} ⊢ {{ P }} e @ E {{ Φ }}.
 Proof. by intros; apply always_mono, impl_mono, wp_mono. Qed.
 Global Instance ht_mono' E :
   Proper (flip (⊢) ==> eq ==> pointwise_relation _ (⊢) ==> (⊢)) (@ht Λ Σ E).
@@ -59,7 +59,7 @@ Lemma ht_val E v : {{ True : iProp Λ Σ }} of_val v @ E {{ v', v = v' }}.
 Proof. iIntros "! _". by iApply wp_value'. Qed.
 
 Lemma ht_vs E P P' Φ Φ' e :
-  ((P ={E}=> P') ∧ {{ P' }} e @ E {{ Φ' }} ∧ ∀ v, Φ' v ={E}=> Φ v)
+  (P ={E}=> P') ∧ {{ P' }} e @ E {{ Φ' }} ∧ (∀ v, Φ' v ={E}=> Φ v)
   ⊢ {{ P }} e @ E {{ Φ }}.
 Proof.
   iIntros "(#Hvs&#Hwp&#HΦ) ! HP". iPvs ("Hvs" with "HP") as "HP".
@@ -69,7 +69,7 @@ Qed.
 
 Lemma ht_atomic E1 E2 P P' Φ Φ' e :
   E2 ⊆ E1 → atomic e →
-  ((P ={E1,E2}=> P') ∧ {{ P' }} e @ E2 {{ Φ' }} ∧ ∀ v, Φ' v ={E2,E1}=> Φ v)
+  (P ={E1,E2}=> P') ∧ {{ P' }} e @ E2 {{ Φ' }} ∧ (∀ v, Φ' v ={E2,E1}=> Φ v)
   ⊢ {{ P }} e @ E1 {{ Φ }}.
 Proof.
   iIntros {??} "(#Hvs&#Hwp&#HΦ) ! HP". iApply (wp_atomic _ E2); auto.
@@ -79,7 +79,7 @@ Proof.
 Qed.
 
 Lemma ht_bind `{LanguageCtx Λ K} E P Φ Φ' e :
-  ({{ P }} e @ E {{ Φ }} ∧ ∀ v, {{ Φ v }} K (of_val v) @ E {{ Φ' }})
+  {{ P }} e @ E {{ Φ }} ∧ (∀ v, {{ Φ v }} K (of_val v) @ E {{ Φ' }})
   ⊢ {{ P }} K e @ E {{ Φ' }}.
 Proof.
   iIntros "(#Hwpe&#HwpK) ! HP". iApply wp_bind.
@@ -104,8 +104,8 @@ Proof. iIntros "#Hwp ! [HP $]". by iApply "Hwp". Qed.
 
 Lemma ht_frame_step_l E E1 E2 P R1 R2 R3 e Φ :
   to_val e = None → E ⊥ E1 → E2 ⊆ E1 →
-  ((R1 ={E1,E2}=> ▷ R2) ∧ (R2 ={E2,E1}=> R3) ∧ {{ P }} e @ E {{ Φ }})
-    ⊢ {{ R1 ★ P }} e @ E ∪ E1 {{ λ v, R3 ★ Φ v }}.
+  (R1 ={E1,E2}=> ▷ R2) ∧ (R2 ={E2,E1}=> R3) ∧ {{ P }} e @ E {{ Φ }}
+  ⊢ {{ R1 ★ P }} e @ E ∪ E1 {{ λ v, R3 ★ Φ v }}.
 Proof.
   iIntros {???} "[#Hvs1 [#Hvs2 #Hwp]] ! [HR HP]".
   iApply (wp_frame_step_l E E1 E2); try done.
@@ -116,8 +116,8 @@ Qed.
 
 Lemma ht_frame_step_r E E1 E2 P R1 R2 R3 e Φ :
   to_val e = None → E ⊥ E1 → E2 ⊆ E1 →
-  ((R1 ={E1,E2}=> ▷ R2) ∧ (R2 ={E2,E1}=> R3) ∧ {{ P }} e @ E {{ Φ }})
-    ⊢ {{ P ★ R1 }} e @ (E ∪ E1) {{ λ v, Φ v ★ R3 }}.
+  (R1 ={E1,E2}=> ▷ R2) ∧ (R2 ={E2,E1}=> R3) ∧ {{ P }} e @ E {{ Φ }}
+  ⊢ {{ P ★ R1 }} e @ (E ∪ E1) {{ λ v, Φ v ★ R3 }}.
 Proof.
   iIntros {???} "[#Hvs1 [#Hvs2 #Hwp]]".
   setoid_rewrite (comm _ _ R3); rewrite (comm _ _ R1).
@@ -142,8 +142,8 @@ Qed.
 
 Lemma ht_inv N E P Φ R e :
   atomic e → nclose N ⊆ E →
-  (inv N R ★ {{ ▷ R ★ P }} e @ E ∖ nclose N {{ v, ▷ R ★ Φ v }})
-    ⊢ {{ P }} e @ E {{ Φ }}.
+  inv N R ★ {{ ▷ R ★ P }} e @ E ∖ nclose N {{ v, ▷ R ★ Φ v }}
+  ⊢ {{ P }} e @ E {{ Φ }}.
 Proof.
   iIntros {??} "[#? #Hwp] ! HP". iInv N as "HR". iApply "Hwp". by iSplitL "HR".
 Qed.
diff --git a/program_logic/hoare_lifting.v b/program_logic/hoare_lifting.v
index 888f08595633b6a7dc92c8d214593084e86a4437..ca9b0ff2ac81403b454cfc3005b8efba65b988d6 100644
--- a/program_logic/hoare_lifting.v
+++ b/program_logic/hoare_lifting.v
@@ -23,10 +23,10 @@ Lemma ht_lift_step E1 E2
   E2 ⊆ E1 → to_val e1 = None →
   reducible e1 σ1 →
   (∀ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → φ e2 σ2 ef) →
-  ((P ={E1,E2}=> ▷ ownP σ1 ★ ▷ P') ∧
+  (P ={E1,E2}=> ▷ ownP σ1 ★ ▷ P') ∧
    (∀ e2 σ2 ef, ■ φ e2 σ2 ef ★ ownP σ2 ★ P' ={E2,E1}=> Φ1 e2 σ2 ef ★ Φ2 e2 σ2 ef) ∧
    (∀ e2 σ2 ef, {{ Φ1 e2 σ2 ef }} e2 @ E1 {{ Ψ }}) ∧
-   (∀ e2 σ2 ef, {{ Φ2 e2 σ2 ef }} ef ?@ ⊤ {{ _, True }}))
+   (∀ e2 σ2 ef, {{ Φ2 e2 σ2 ef }} ef ?@ ⊤ {{ _, True }})
   ⊢ {{ P }} e1 @ E1 {{ Ψ }}.
 Proof.
   iIntros {?? Hsafe Hstep} "#(#Hvs&HΦ&He2&Hef) ! HP".
@@ -67,8 +67,8 @@ Lemma ht_lift_pure_step E (φ : expr Λ → option (expr Λ) → Prop) P P' Ψ e
   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 ★ P }} e2 @ E {{ Ψ }}) ∧
-   (∀ e2 ef, {{ ■ φ e2 ef ★ P' }} ef ?@ ⊤ {{ _, True }}))
+  (∀ e2 ef, {{ ■ φ e2 ef ★ P }} e2 @ E {{ Ψ }}) ∧
+    (∀ e2 ef, {{ ■ φ e2 ef ★ P' }} ef ?@ ⊤ {{ _, True }})
   ⊢ {{ ▷(P ★ P') }} e1 @ E {{ Ψ }}.
 Proof.
   iIntros {? Hsafe Hstep} "[#He2 #Hef] ! HP".
@@ -84,7 +84,7 @@ Lemma ht_lift_pure_det_step
   to_val e1 = None →
   (∀ σ1, reducible e1 σ1) →
   (∀ σ1 e2' σ2 ef', prim_step e1 σ1 e2' σ2 ef' → σ1 = σ2 ∧ e2 = e2' ∧ ef = ef')→
-  ({{ P }} e2 @ E {{ Ψ }} ∧ {{ P' }} ef ?@ ⊤ {{ _, True }})
+  {{ P }} e2 @ E {{ Ψ }} ∧ {{ P' }} ef ?@ ⊤ {{ _, True }}
   ⊢ {{ ▷(P ★ P') }} e1 @ E {{ Ψ }}.
 Proof.
   iIntros {? Hsafe Hdet} "[#He2 #Hef]".
diff --git a/program_logic/invariants.v b/program_logic/invariants.v
index 0eeeed950d8a485d5e11e3b1c757c980b4c4772f..10f57adee165447f2db131a698f7522f1918d34f 100644
--- a/program_logic/invariants.v
+++ b/program_logic/invariants.v
@@ -49,7 +49,7 @@ Qed.
     verbose to apply than [inv_open]. *)
 Lemma inv_fsa {A} (fsa : FSA Λ Σ A) `{!FrameShiftAssertion fsaV fsa} E N P Ψ :
   fsaV → nclose N ⊆ E →
-  (inv N P ★ (▷ P -★ fsa (E ∖ nclose N) (λ a, ▷ P ★ Ψ a))) ⊢ fsa E Ψ.
+  inv N P ★ (▷ P -★ fsa (E ∖ nclose N) (λ a, ▷ P ★ Ψ a)) ⊢ fsa E Ψ.
 Proof.
   iIntros {??} "[Hinv HΨ]".
   iDestruct (inv_open E N P with "Hinv") as {E'} "[% Hvs]"; first done.
diff --git a/program_logic/lifting.v b/program_logic/lifting.v
index 1db2f04ff59db93448c93d716e942e218944aefc..d2b80d543ab41b0252bbad79061d6f29f011da1a 100644
--- a/program_logic/lifting.v
+++ b/program_logic/lifting.v
@@ -66,7 +66,7 @@ Lemma wp_lift_atomic_step {E Φ} e1
   reducible e1 σ1 →
   (∀ e2 σ2 ef,
     prim_step e1 σ1 e2 σ2 ef → φ e2 σ2 ef) →
-  (▷ ownP σ1 ★ ▷ ∀ v2 σ2 ef, ■ φ (of_val v2) σ2 ef ∧ ownP σ2 -★ Φ v2 ★ wp_fork ef)
+  ▷ ownP σ1 ★ ▷ (∀ v2 σ2 ef, ■ φ (of_val v2) σ2 ef ∧ ownP σ2 -★ Φ v2 ★ wp_fork ef)
   ⊢ WP e1 @ E {{ Φ }}.
 Proof.
   intros. rewrite -(wp_lift_step E E (λ e2 σ2 ef,
@@ -88,7 +88,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 e1 @ E {{ Φ }}.
+  ▷ ownP σ1 ★ ▷ (ownP σ2 -★ Φ v2 ★ wp_fork ef) ⊢ WP e1 @ E {{ Φ }}.
 Proof.
   intros. rewrite -(wp_lift_atomic_step _ (λ e2' σ2' ef',
     σ2 = σ2' ∧ to_val e2' = Some v2 ∧ ef = ef') σ1) //.
@@ -110,5 +110,4 @@ Proof.
   apply later_mono, forall_intro=>e'; apply forall_intro=>ef'.
   by apply impl_intro_l, const_elim_l=>-[-> ->].
 Qed.
-
 End lifting.
diff --git a/program_logic/ownership.v b/program_logic/ownership.v
index 88368a6cf5ec4529a8225f835008e65fa469271d..f7dfc25aad62c7a9991dbb34c527da90dde88a9a 100644
--- a/program_logic/ownership.v
+++ b/program_logic/ownership.v
@@ -29,7 +29,7 @@ Global Instance ownI_persistent i P : PersistentP (ownI i P).
 Proof. rewrite /ownI. apply _. Qed.
 
 (* physical state *)
-Lemma ownP_twice σ1 σ2 : (ownP σ1 ★ ownP σ2 : iProp Λ Σ) ⊢ False.
+Lemma ownP_twice σ1 σ2 : ownP σ1 ★ ownP σ2 ⊢ (False : iProp Λ Σ).
 Proof.
   rewrite /ownP -uPred.ownM_op Res_op.
   by apply uPred.ownM_invalid; intros (_&?&_).
@@ -41,13 +41,13 @@ Proof. rewrite /ownP; apply _. Qed.
 Global Instance ownG_ne n : Proper (dist n ==> dist n) (@ownG Λ Σ).
 Proof. solve_proper. Qed.
 Global Instance ownG_proper : Proper ((≡) ==> (⊣⊢)) (@ownG Λ Σ) := ne_proper _.
-Lemma ownG_op m1 m2 : ownG (m1 ⋅ m2) ⊣⊢ (ownG m1 ★ ownG m2).
+Lemma ownG_op m1 m2 : ownG (m1 ⋅ m2) ⊣⊢ ownG m1 ★ ownG m2.
 Proof. by rewrite /ownG -uPred.ownM_op Res_op !left_id. Qed.
 Global Instance ownG_mono : Proper (flip (≼) ==> (⊢)) (@ownG Λ Σ).
 Proof. move=>a b [c H]. rewrite H ownG_op. eauto with I. Qed.
 Lemma ownG_valid m : ownG m ⊢ ✓ m.
 Proof. rewrite /ownG uPred.ownM_valid res_validI /=; auto with I. Qed.
-Lemma ownG_valid_r m : ownG m ⊢ (ownG m ★ ✓ m).
+Lemma ownG_valid_r m : ownG m ⊢ ownG m ★ ✓ m.
 Proof. apply (uPred.always_entails_r _ _), ownG_valid. Qed.
 Lemma ownG_empty : True ⊢ (ownG ∅ : iProp Λ Σ).
 Proof. apply: uPred.ownM_empty. Qed.
diff --git a/program_logic/pviewshifts.v b/program_logic/pviewshifts.v
index 853df60b4df459ccd375eed0e981f0d6bb2d6680..3aaa3521ab0ad958666134c36f34e89b241cf6ef 100644
--- a/program_logic/pviewshifts.v
+++ b/program_logic/pviewshifts.v
@@ -70,7 +70,7 @@ Proof.
   rewrite pvs_eq. split=> n r ? HP rf k Ef σ ???; exists r; split; last done.
   apply uPred_closed with n; eauto.
 Qed.
-Lemma pvs_mono E1 E2 P Q : P ⊢ Q → (|={E1,E2}=> P) ={E1,E2}=> Q.
+Lemma pvs_mono E1 E2 P Q : (P ⊢ Q) → (|={E1,E2}=> P) ={E1,E2}=> Q.
 Proof.
   rewrite pvs_eq. intros HPQ; split=> n r ? HP rf k Ef σ ???.
   destruct (HP rf k Ef σ) as (r2&?&?); eauto.
@@ -157,7 +157,7 @@ Proof. move=>->. by rewrite pvs_trans'. Qed.
 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 `{!PersistentP P} :
-  (P ∧ |={E1,E2}=> Q) ={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 `{!PersistentP Q} :
   (|={E1,E2}=> P) ∧ Q ={E1,E2}=> P ∧ Q.
@@ -201,7 +201,7 @@ Proof. intros. etrans. apply pvs_closeI. apply pvs_mask_frame'; set_solver. Qed.
 
 Lemma pvs_mask_frame_mono E1 E1' E2 E2' P Q :
   E1' ⊆ E1 → E2' ⊆ E2 → E1 ∖ E1' = E2 ∖ E2' →
-  P ⊢ Q → (|={E1',E2'}=> P) ={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
@@ -247,9 +247,9 @@ Lemma fsa_mono E Φ Ψ : (∀ a, Φ a ⊢ Ψ a) → fsa E Φ ⊢ fsa E Ψ.
 Proof. apply fsa_mask_frame_mono; auto. Qed.
 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).
+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 Φ → (|={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.
@@ -263,12 +263,12 @@ Proof.
 Qed.
 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.
-Lemma fsa_wand_l E Φ Ψ : ((∀ a, Φ a -★ Ψ a) ★ fsa E Φ) ⊢ fsa E Ψ.
+Lemma fsa_wand_l E Φ Ψ : (∀ a, Φ a -★ Ψ a) ★ fsa E Φ ⊢ fsa E Ψ.
 Proof.
   rewrite fsa_frame_l. apply fsa_mono=> a.
   by rewrite (forall_elim a) wand_elim_l.
 Qed.
-Lemma fsa_wand_r E Φ Ψ : (fsa E Φ ★ ∀ a, Φ a -★ Ψ a) ⊢ fsa E Ψ.
+Lemma fsa_wand_r E Φ Ψ : fsa E Φ ★ (∀ a, Φ a -★ Ψ a) ⊢ fsa E Ψ.
 Proof. by rewrite (comm _ (fsa _ _)) fsa_wand_l. Qed.
 End fsa.
 
diff --git a/program_logic/resources.v b/program_logic/resources.v
index 0304c1bc0c554953fbe4e84d533a52b5a3cf416b..b12df6173c90aab79155eb1b6bc57f8bd210b5a0 100644
--- a/program_logic/resources.v
+++ b/program_logic/resources.v
@@ -163,12 +163,11 @@ Proof. do 2 constructor; apply (persistent_core _). Qed.
 
 (** Internalized properties *)
 Lemma res_equivI {M'} r1 r2 :
-  (r1 ≡ r2)
-  ⊣⊢ (wld r1 ≡ wld r2 ∧ pst r1 ≡ pst r2 ∧ gst r1 ≡ gst r2: uPred M').
+  r1 ≡ r2 ⊣⊢ (wld r1 ≡ wld r2 ∧ pst r1 ≡ pst r2 ∧ gst r1 ≡ gst r2 : uPred M').
 Proof.
   uPred.unseal. do 2 split. by destruct 1. by intros (?&?&?); by constructor.
 Qed.
-Lemma res_validI {M'} r : (✓ r) ⊣⊢ (✓ wld r ∧ ✓ pst r ∧ ✓ gst r : uPred M').
+Lemma res_validI {M'} r : ✓ r ⊣⊢ (✓ wld r ∧ ✓ pst r ∧ ✓ gst r : uPred M').
 Proof. by uPred.unseal. Qed.
 End res.
 
diff --git a/program_logic/saved_one_shot.v b/program_logic/saved_one_shot.v
index 8ada91cfa99c7e39f7a8df4a4238a3007bd93576..be0f838ffca722eb6cc4005e2857ee9583f66e8f 100644
--- a/program_logic/saved_one_shot.v
+++ b/program_logic/saved_one_shot.v
@@ -42,7 +42,7 @@ Section one_shot.
     apply one_shot_init.
   Qed.
 
-  Lemma one_shot_agree γ x y : (one_shot_own γ x ★ one_shot_own γ y) ⊢ ▷(x ≡ y).
+  Lemma one_shot_agree γ x y : one_shot_own γ x ★ one_shot_own γ y ⊢ ▷ (x ≡ y).
   Proof.
     rewrite -own_op own_valid one_shot_validI /= agree_validI.
     rewrite agree_equivI later_equivI.
diff --git a/program_logic/saved_prop.v b/program_logic/saved_prop.v
index ccbe15a8817d821bc6fe907fd3bc3754250b66b8..b369d833282c957d2190011fef908d0cd6c6d0a3 100644
--- a/program_logic/saved_prop.v
+++ b/program_logic/saved_prop.v
@@ -31,7 +31,7 @@ Section saved_prop.
   Proof. by apply own_alloc. Qed.
 
   Lemma saved_prop_agree γ x y :
-    (saved_prop_own γ x ★ saved_prop_own γ y) ⊢ ▷(x ≡ y).
+    saved_prop_own γ x ★ saved_prop_own γ y ⊢ ▷ (x ≡ y).
   Proof.
     rewrite -own_op own_valid agree_validI agree_equivI later_equivI.
     set (G1 := cFunctor_map F (iProp_fold, iProp_unfold)).
diff --git a/program_logic/sts.v b/program_logic/sts.v
index 36307b1ca24c10369167db6734edd4cc4e2c9804..25eb24bd2b16cc015978447256034455118d1d81 100644
--- a/program_logic/sts.v
+++ b/program_logic/sts.v
@@ -93,7 +93,7 @@ Section sts.
 
   Lemma sts_fsaS E N (Ψ : V → iPropG Λ Σ) γ S T :
     fsaV → nclose N ⊆ E →
-    (sts_ctx γ N φ ★ sts_ownS γ S T ★ ∀ s,
+    sts_ctx γ N φ ★ sts_ownS γ S T ★ (∀ s,
       ■ (s ∈ S) ★ ▷ φ s -★
       fsa (E ∖ nclose N) (λ x, ∃ s' T',
         ■ sts.steps (s, T) (s', T') ★ ▷ φ s' ★ (sts_own γ s' T' -★ Ψ x)))
@@ -116,7 +116,7 @@ Section sts.
 
   Lemma sts_fsa E N (Ψ : V → iPropG Λ Σ) γ s0 T :
     fsaV → nclose N ⊆ E →
-    (sts_ctx γ N φ ★ sts_own γ s0 T ★ ∀ s,
+    sts_ctx γ N φ ★ sts_own γ s0 T ★ (∀ s,
       ■ (s ∈ sts.up s0 T) ★ ▷ φ s -★
       fsa (E ∖ nclose N) (λ x, ∃ s' T',
         ■ (sts.steps (s, T) (s', T')) ★ ▷ φ s' ★
diff --git a/program_logic/viewshifts.v b/program_logic/viewshifts.v
index 37866af4403a4c375115faabb0edeafa43bf0ab6..c8a39cf0d3e2f1dac5a4d41e8b165c98425a769b 100644
--- a/program_logic/viewshifts.v
+++ b/program_logic/viewshifts.v
@@ -27,7 +27,7 @@ Global Instance vs_proper E1 E2 : Proper ((≡) ==> (≡) ==> (≡)) (@vs Λ Σ
 Proof. apply ne_proper_2, _. Qed.
 
 Lemma vs_mono E1 E2 P P' Q Q' :
-  P ⊢ P' → Q' ⊢ Q → (P' ={E1,E2}=> Q') ⊢ (P ={E1,E2}=> Q).
+  (P ⊢ P') → (Q' ⊢ Q) → (P' ={E1,E2}=> Q') ⊢ P ={E1,E2}=> Q.
 Proof. by intros HP HQ; rewrite /vs -HP HQ. Qed.
 
 Global Instance vs_mono' E1 E2 :
@@ -40,37 +40,37 @@ Lemma vs_timeless E P : TimelessP P → ▷ P ={E}=> P.
 Proof. by apply pvs_timeless. Qed.
 
 Lemma vs_transitive E1 E2 E3 P Q R :
-  E2 ⊆ E1 ∪ E3 → ((P ={E1,E2}=> Q) ∧ (Q ={E2,E3}=> R)) ⊢ (P ={E1,E3}=> R).
+  E2 ⊆ E1 ∪ E3 → (P ={E1,E2}=> Q) ∧ (Q ={E2,E3}=> R) ⊢ P ={E1,E3}=> R.
 Proof.
   iIntros {?} "#[HvsP HvsQ] ! HP".
   iPvs ("HvsP" with "HP") as "HQ"; first done. by iApply "HvsQ".
 Qed.
 
-Lemma vs_transitive' E P Q R : ((P ={E}=> Q) ∧ (Q ={E}=> R)) ⊢ (P ={E}=> R).
+Lemma vs_transitive' E P Q R : (P ={E}=> Q) ∧ (Q ={E}=> R) ⊢ (P ={E}=> R).
 Proof. apply vs_transitive; set_solver. Qed.
 Lemma vs_reflexive E P : P ={E}=> P.
 Proof. by iIntros "HP". Qed.
 
-Lemma vs_impl E P Q : □ (P → Q) ⊢ (P ={E}=> Q).
+Lemma vs_impl E P Q : □ (P → Q) ⊢ P ={E}=> Q.
 Proof. iIntros "#HPQ ! HP". by iApply "HPQ". Qed.
 
-Lemma vs_frame_l E1 E2 P Q R : (P ={E1,E2}=> Q) ⊢ (R ★ P ={E1,E2}=> R ★ Q).
+Lemma vs_frame_l E1 E2 P Q R : (P ={E1,E2}=> Q) ⊢ R ★ P ={E1,E2}=> R ★ Q.
 Proof. iIntros "#Hvs ! [$ HP]". by iApply "Hvs". Qed.
 
-Lemma vs_frame_r E1 E2 P Q R : (P ={E1,E2}=> Q) ⊢ (P ★ R ={E1,E2}=> Q ★ R).
+Lemma vs_frame_r E1 E2 P Q R : (P ={E1,E2}=> Q) ⊢ P ★ R ={E1,E2}=> Q ★ R.
 Proof. iIntros "#Hvs ! [HP $]". by iApply "Hvs". Qed.
 
 Lemma vs_mask_frame E1 E2 Ef P Q :
-  Ef ⊥ E1 ∪ E2 → (P ={E1,E2}=> Q) ⊢ (P ={E1 ∪ Ef,E2 ∪ Ef}=> Q).
+  Ef ⊥ E1 ∪ E2 → (P ={E1,E2}=> Q) ⊢ P ={E1 ∪ Ef,E2 ∪ Ef}=> Q.
 Proof.
   iIntros {?} "#Hvs ! HP". iApply pvs_mask_frame; auto. by iApply "Hvs".
 Qed.
 
-Lemma vs_mask_frame' E Ef P Q : Ef ⊥ E → (P ={E}=> Q) ⊢ (P ={E ∪ Ef}=> Q).
+Lemma vs_mask_frame' E Ef P Q : Ef ⊥ E → (P ={E}=> Q) ⊢ P ={E ∪ Ef}=> Q.
 Proof. intros; apply vs_mask_frame; set_solver. Qed.
 
 Lemma vs_inv N E P Q R :
-  nclose N ⊆ E → (inv N R ★ (▷ R ★ P ={E ∖ nclose N}=> ▷ R ★ Q)) ⊢ (P ={E}=> Q).
+  nclose N ⊆ E → inv N R ★ (▷ R ★ P ={E ∖ nclose N}=> ▷ R ★ Q) ⊢ P ={E}=> Q.
 Proof.
   iIntros {?} "#[? Hvs] ! HP". iInv N as "HR". iApply "Hvs". by iSplitL "HR".
 Qed.
diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index 74bea5bc88709fd1e10831d43e6ef41c81d28404..443f64257c40cc1206fc23f31eb56ea8ffc341b2 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -120,8 +120,7 @@ Proof.
     exact: pvs_zero.
   - constructor; first done. intros ?????. exfalso. omega.
 Qed.
-Lemma wp_value_inv E Φ v n r :
-  wp_def E (of_val v) Φ n r → pvs E E (Φ v) n r.
+Lemma wp_value_inv E Φ v n r : wp_def E (of_val v) Φ n r → pvs E E (Φ v) n r.
 Proof.
   by inversion 1 as [|??? He]; [|rewrite ?to_of_val in He]; simplify_eq.
 Qed.
@@ -145,7 +144,7 @@ Proof.
   rewrite pvs_eq in Hvs. destruct (Hvs rf (S k) Ef σ1) as (r'&Hwp&?); auto.
   eapply wp_step_inv with (S k) r'; eauto.
 Qed.
-Lemma wp_pvs E e Φ : WP e @  E {{ v, |={E}=> Φ v }} ⊢ WP e @ E {{ Φ }}.
+Lemma wp_pvs E e Φ : WP e @ E {{ v, |={E}=> Φ v }} ⊢ WP e @ E {{ Φ }}.
 Proof.
   rewrite wp_eq. split=> n r; revert e r;
     induction n as [n IH] using lt_wf_ind=> e r Hr HΦ.
@@ -176,7 +175,7 @@ Proof.
   - by rewrite -assoc.
   - constructor; apply pvs_intro; auto.
 Qed.
-Lemma wp_frame_r E e Φ R : (WP e @ E {{ Φ }} ★ R) ⊢ WP e @ E {{ v, Φ v ★ R }}.
+Lemma wp_frame_r E e Φ R : WP e @ E {{ Φ }} ★ R ⊢ WP e @ E {{ v, Φ v ★ R }}.
 Proof.
   rewrite wp_eq. uPred.unseal; split; intros n r' Hvalid (r&rR&Hr&Hwp&?).
   revert Hvalid. rewrite Hr; clear Hr; revert e r Hwp.
@@ -195,7 +194,7 @@ Proof.
 Qed.
 Lemma wp_frame_step_r E E1 E2 e Φ R :
   to_val e = None → E ⊥ E1 → E2 ⊆ E1 →
-    (WP e @ E {{ Φ }} ★ |={E1,E2}=> ▷ |={E2,E1}=> R)
+  WP e @ E {{ Φ }} ★ (|={E1,E2}=> ▷ |={E2,E1}=> R)
   ⊢ WP e @ E ∪ E1 {{ v, Φ v ★ R }}.
 Proof.
   rewrite wp_eq pvs_eq=> He ??.
@@ -254,17 +253,17 @@ 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 {{ Φ }}.
+  (P ⊢ WP e @ E {{ Φ }}) → (|={E}=> P) ⊢ WP e @ E {{ Φ }}.
 Proof. move=>->. by rewrite pvs_wp. Qed.
 Lemma wp_value E Φ e v : to_val e = Some v → Φ v ⊢ WP 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 {{ Φ }}.
 Proof. intros. rewrite -wp_pvs. rewrite -wp_value //. Qed.
-Lemma wp_frame_l E e Φ R : (R ★ WP e @ E {{ Φ }}) ⊢ WP e @ E {{ v, R ★ Φ v }}.
+Lemma wp_frame_l E e Φ R : R ★ WP e @ E {{ Φ }} ⊢ WP e @ E {{ v, R ★ Φ v }}.
 Proof. setoid_rewrite (comm _ R); apply wp_frame_r. Qed.
 Lemma wp_frame_step_r' E e Φ R :
-  to_val e = None → (WP e @ E {{ Φ }} ★ ▷ R) ⊢ WP e @ E {{ v, Φ v ★ R }}.
+  to_val e = None → WP e @ E {{ Φ }} ★ ▷ R ⊢ WP e @ E {{ v, Φ v ★ R }}.
 Proof.
   intros. rewrite {2}(_ : E = E ∪ ∅); last by set_solver.
   rewrite -(wp_frame_step_r E ∅ ∅); [|auto|set_solver..].
@@ -272,31 +271,31 @@ Proof.
 Qed.
 Lemma wp_frame_step_l E E1 E2 e Φ R :
   to_val e = None → E ⊥ E1 → E2 ⊆ E1 →
-  ((|={E1,E2}=> ▷ |={E2,E1}=> R) ★ WP e @ E {{ Φ }})
+  (|={E1,E2}=> ▷ |={E2,E1}=> R) ★ WP e @ E {{ Φ }}
   ⊢ WP e @ (E ∪ E1) {{ v, R ★ Φ v }}.
 Proof.
   rewrite [((|={E1,E2}=> _) ★ _)%I]comm; setoid_rewrite (comm _ R).
   apply wp_frame_step_r.
 Qed.
 Lemma wp_frame_step_l' E e Φ R :
-  to_val e = None → (▷ R ★ WP e @ E {{ Φ }}) ⊢ WP e @ E {{ v, R ★ Φ v }}.
+  to_val e = None → ▷ R ★ WP e @ E {{ Φ }} ⊢ WP e @ E {{ v, R ★ Φ v }}.
 Proof.
   rewrite (comm _ (â–· R)%I); setoid_rewrite (comm _ R).
   apply wp_frame_step_r'.
 Qed.
 Lemma wp_always_l E e Φ R `{!PersistentP R} :
-  (R ∧ WP e @ E {{ Φ }}) ⊢ WP e @ E {{ v, R ∧ Φ v }}.
+  R ∧ WP e @ E {{ Φ }} ⊢ WP e @ E {{ v, R ∧ Φ v }}.
 Proof. by setoid_rewrite (always_and_sep_l _ _); rewrite wp_frame_l. Qed.
 Lemma wp_always_r E e Φ R `{!PersistentP R} :
-  (WP e @ E {{ Φ }} ∧ R) ⊢ WP e @ E {{ v, Φ v ∧ R }}.
+  WP e @ E {{ Φ }} ∧ R ⊢ WP e @ E {{ v, Φ v ∧ R }}.
 Proof. by setoid_rewrite (always_and_sep_r _ _); rewrite wp_frame_r. Qed.
 Lemma wp_wand_l E e Φ Ψ :
-  ((∀ v, Φ v -★ Ψ v) ★ WP e @ E {{ Φ }}) ⊢ WP e @ E {{ Ψ }}.
+  (∀ v, Φ v -★ Ψ v) ★ WP e @ E {{ Φ }} ⊢ WP e @ E {{ Ψ }}.
 Proof.
   rewrite wp_frame_l. apply wp_mono=> v. by rewrite (forall_elim v) wand_elim_l.
 Qed.
 Lemma wp_wand_r E e Φ Ψ :
-  (WP e @ E {{ Φ }} ★ (∀ v, Φ v -★ Ψ v)) ⊢ WP e @ E {{ Ψ }}.
+  WP e @ E {{ Φ }} ★ (∀ v, Φ v -★ Ψ v) ⊢ WP e @ E {{ Ψ }}.
 Proof. by rewrite comm wp_wand_l. Qed.
 
 Lemma wp_mask_weaken E1 E2 e Φ :
diff --git a/proofmode/coq_tactics.v b/proofmode/coq_tactics.v
index 4990d7bf4a70b2ec00fcf41441e74e20e96cef06..cb2349e671d261a1473accee2843b132ff1e875e 100644
--- a/proofmode/coq_tactics.v
+++ b/proofmode/coq_tactics.v
@@ -115,7 +115,7 @@ Proof.
 Qed.
 
 Lemma envs_lookup_sound Δ i p P :
-  envs_lookup i Δ = Some (p,P) → Δ ⊢ (□?p P ★ envs_delete i p Δ).
+  envs_lookup i Δ = Some (p,P) → Δ ⊢ □?p P ★ envs_delete i p Δ.
 Proof.
   rewrite /envs_lookup /envs_delete /of_envs=>?; apply const_elim_sep_l=> Hwf.
   destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
@@ -130,16 +130,16 @@ Proof.
       naive_solver eauto using env_delete_wf, env_delete_fresh.
 Qed.
 Lemma envs_lookup_sound' Δ i p P :
-  envs_lookup i Δ = Some (p,P) → Δ ⊢ (P ★ envs_delete i p Δ).
+  envs_lookup i Δ = Some (p,P) → Δ ⊢ P ★ envs_delete i p Δ.
 Proof. intros. rewrite envs_lookup_sound //. by rewrite always_if_elim. Qed.
 Lemma envs_lookup_persistent_sound Δ i P :
-  envs_lookup i Δ = Some (true,P) → Δ ⊢ (□ P ★ Δ).
+  envs_lookup i Δ = Some (true,P) → Δ ⊢ □ P ★ Δ.
 Proof.
   intros. apply: always_entails_l. by rewrite envs_lookup_sound // sep_elim_l.
 Qed.
 
 Lemma envs_lookup_split Δ i p P :
-  envs_lookup i Δ = Some (p,P) → Δ ⊢ (□?p P ★ (□?p P -★ Δ)).
+  envs_lookup i Δ = Some (p,P) → Δ ⊢ □?p P ★ (□?p P -★ Δ).
 Proof.
   rewrite /envs_lookup /of_envs=>?; apply const_elim_sep_l=> Hwf.
   destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
@@ -152,13 +152,13 @@ Proof.
 Qed.
 
 Lemma envs_lookup_delete_sound Δ Δ' i p P :
-  envs_lookup_delete i Δ = Some (p,P,Δ') → Δ ⊢ (□?p P ★ Δ')%I.
+  envs_lookup_delete i Δ = Some (p,P,Δ') → Δ ⊢ □?p P ★ Δ'.
 Proof. intros [? ->]%envs_lookup_delete_Some. by apply envs_lookup_sound. Qed.
 Lemma envs_lookup_delete_sound' Δ Δ' i p P :
-  envs_lookup_delete i Δ = Some (p,P,Δ') → Δ ⊢ (P ★ Δ')%I.
+  envs_lookup_delete i Δ = Some (p,P,Δ') → Δ ⊢ P ★ Δ'.
 Proof. intros [? ->]%envs_lookup_delete_Some. by apply envs_lookup_sound'. Qed.
 
-Lemma envs_app_sound Δ Δ' p Γ : envs_app p Γ Δ = Some Δ' → Δ ⊢ (□?p [★] Γ -★ Δ').
+Lemma envs_app_sound Δ Δ' p Γ : envs_app p Γ Δ = Some Δ' → Δ ⊢ □?p [★] Γ -★ Δ'.
 Proof.
   rewrite /of_envs /envs_app=> ?; apply const_elim_sep_l=> Hwf.
   destruct Δ as [Γp Γs], p; simplify_eq/=.
@@ -182,7 +182,7 @@ Qed.
 
 Lemma envs_simple_replace_sound' Δ Δ' i p Γ :
   envs_simple_replace i p Γ Δ = Some Δ' →
-  envs_delete i p Δ ⊢ (□?p [★] Γ -★ Δ')%I.
+  envs_delete i p Δ ⊢ □?p [★] Γ -★ Δ'.
 Proof.
   rewrite /envs_simple_replace /envs_delete /of_envs=> ?.
   apply const_elim_sep_l=> Hwf. destruct Δ as [Γp Γs], p; simplify_eq/=.
@@ -206,11 +206,11 @@ Qed.
 
 Lemma envs_simple_replace_sound Δ Δ' i p P Γ :
   envs_lookup i Δ = Some (p,P) → envs_simple_replace i p Γ Δ = Some Δ' →
-  Δ ⊢ (□?p P ★ (□?p [★] Γ -★ Δ'))%I.
+  Δ ⊢ □?p P ★ (□?p [★] Γ -★ Δ').
 Proof. intros. by rewrite envs_lookup_sound// envs_simple_replace_sound'//. Qed.
 
 Lemma envs_replace_sound' Δ Δ' i p q Γ :
-  envs_replace i p q Γ Δ = Some Δ' → envs_delete i p Δ ⊢ (□?q [★] Γ -★ Δ')%I.
+  envs_replace i p q Γ Δ = Some Δ' → envs_delete i p Δ ⊢ □?q [★] Γ -★ Δ'.
 Proof.
   rewrite /envs_replace; destruct (eqb _ _) eqn:Hpq.
   - apply eqb_prop in Hpq as ->. apply envs_simple_replace_sound'.
@@ -219,11 +219,11 @@ Qed.
 
 Lemma envs_replace_sound Δ Δ' i p q P Γ :
   envs_lookup i Δ = Some (p,P) → envs_replace i p q Γ Δ = Some Δ' →
-  Δ ⊢ (□?p P ★ (□?q [★] Γ -★ Δ'))%I.
+  Δ ⊢ □?p P ★ (□?q [★] Γ -★ Δ').
 Proof. intros. by rewrite envs_lookup_sound// envs_replace_sound'//. Qed.
 
 Lemma envs_split_sound Δ lr js Δ1 Δ2 :
-  envs_split lr js Δ = Some (Δ1,Δ2) → Δ ⊢ (Δ1 ★ Δ2).
+  envs_split lr js Δ = Some (Δ1,Δ2) → Δ ⊢ Δ1 ★ Δ2.
 Proof.
   rewrite /envs_split /of_envs=> ?; apply const_elim_sep_l=> Hwf.
   destruct Δ as [Γp Γs], (env_split js _) as [[Γs1 Γs2]|] eqn:?; simplify_eq/=.
@@ -234,8 +234,7 @@ Proof.
       env_split_fresh_1, env_split_fresh_2.
 Qed.
 
-Lemma envs_clear_spatial_sound Δ :
-  Δ ⊢ (envs_clear_spatial Δ ★ [★] env_spatial Δ)%I.
+Lemma envs_clear_spatial_sound Δ : Δ ⊢ envs_clear_spatial Δ ★ [★] env_spatial Δ.
 Proof.
   rewrite /of_envs /envs_clear_spatial /=; apply const_elim_sep_l=> Hwf.
   rewrite right_id -assoc; apply sep_intro_True_l; [apply const_intro|done].
@@ -286,7 +285,7 @@ Global Instance Envs_mono (R : relation (uPred M)) :
 Proof. by constructor. Qed.
 
 (** * Adequacy *)
-Lemma tac_adequate P : Envs Enil Enil ⊢ P → True ⊢ P.
+Lemma tac_adequate P : (Envs Enil Enil ⊢ P) → True ⊢ P.
 Proof.
   intros <-. rewrite /of_envs /= always_const !right_id.
   apply const_intro; repeat constructor.
@@ -311,20 +310,20 @@ Proof. intros. by rewrite envs_lookup_sound // sep_elim_l. Qed.
 Lemma tac_rename Δ Δ' i j p P Q :
   envs_lookup i Δ = Some (p,P) →
   envs_simple_replace i p (Esnoc Enil j P) Δ = Some Δ' →
-  Δ' ⊢ Q → Δ ⊢ Q.
+  (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
   intros. rewrite envs_simple_replace_sound //.
   destruct p; simpl; by rewrite right_id wand_elim_r.
 Qed.
 Lemma tac_clear Δ Δ' i p P Q :
-  envs_lookup_delete i Δ = Some (p,P,Δ') → Δ' ⊢ Q → Δ ⊢ Q.
+  envs_lookup_delete i Δ = Some (p,P,Δ') → (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof. intros. by rewrite envs_lookup_delete_sound // sep_elim_r. Qed.
 Lemma tac_clear_spatial Δ Δ' Q :
-  envs_clear_spatial Δ = Δ' → Δ' ⊢ Q → Δ ⊢ Q.
+  envs_clear_spatial Δ = Δ' → (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof. intros <- ?. by rewrite envs_clear_spatial_sound // sep_elim_l. Qed.
 
 (** * False *)
-Lemma tac_ex_falso Δ Q : Δ ⊢ False → Δ ⊢ Q.
+Lemma tac_ex_falso Δ Q : (Δ ⊢ False) → Δ ⊢ Q.
 Proof. by rewrite -(False_elim Q). Qed.
 
 (** * Pure *)
@@ -349,7 +348,7 @@ Proof.
   rewrite (to_pure P); by apply const_elim_sep_l.
 Qed.
 
-Lemma tac_pure_revert Δ φ Q : Δ ⊢ (■ φ → Q) → (φ → Δ ⊢ Q).
+Lemma tac_pure_revert Δ φ Q : (Δ ⊢ ■ φ → Q) → (φ → Δ ⊢ Q).
 Proof. intros HΔ ?. by rewrite HΔ const_equiv // left_id. Qed.
 
 (** * Later *)
@@ -381,13 +380,13 @@ Proof.
 Qed.
 
 Lemma tac_next Δ Δ' Q Q' :
-  StripLaterEnvs Δ Δ' → StripLaterL Q Q' → Δ' ⊢ Q' → Δ ⊢ Q.
+  StripLaterEnvs Δ Δ' → StripLaterL Q Q' → (Δ' ⊢ Q') → Δ ⊢ Q.
 Proof. intros ?? HQ. by rewrite -(strip_later_l Q) strip_later_env_sound HQ. Qed.
 
 Lemma tac_löb Δ Δ' i Q :
   envs_persistent Δ = true →
   envs_app true (Esnoc Enil i (▷ Q)%I) Δ = Some Δ' →
-  Δ' ⊢ Q → Δ ⊢ Q.
+  (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
   intros ?? HQ. rewrite -(always_elim Q) -(löb (□ Q)) -always_later.
   apply impl_intro_l, (always_intro _ _).
@@ -396,7 +395,7 @@ Proof.
 Qed.
 
 (** * Always *)
-Lemma tac_always_intro Δ Q : envs_persistent Δ = true → Δ ⊢ Q → Δ ⊢ □ Q.
+Lemma tac_always_intro Δ Q : envs_persistent Δ = true → (Δ ⊢ Q) → Δ ⊢ □ Q.
 Proof. intros. by apply: always_intro. Qed.
 
 Class ToPersistentP (P Q : uPred M) := to_persistentP : P ⊢ □ Q.
@@ -413,7 +412,7 @@ Proof. done. Qed.
 Lemma tac_persistent Δ Δ' i p P P' Q :
   envs_lookup i Δ = Some (p, P) → ToPersistentP P P' →
   envs_replace i p true (Esnoc Enil i P') Δ = Some Δ' →
-  Δ' ⊢ Q → Δ ⊢ Q.
+  (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
   intros ??? <-. rewrite envs_replace_sound //; simpl.
   by rewrite right_id (to_persistentP P) always_if_always wand_elim_r.
@@ -423,7 +422,7 @@ Qed.
 Lemma tac_impl_intro Δ Δ' i P Q :
   envs_persistent Δ = true →
   envs_app false (Esnoc Enil i P) Δ = Some Δ' →
-  Δ' ⊢ Q → Δ ⊢ (P → Q).
+  (Δ' ⊢ Q) → Δ ⊢ P → Q.
 Proof.
   intros ?? HQ. rewrite (persistentP Δ) envs_app_sound //; simpl.
   by rewrite right_id always_wand_impl always_elim HQ.
@@ -431,35 +430,35 @@ Qed.
 Lemma tac_impl_intro_persistent Δ Δ' i P P' Q :
   ToPersistentP P P' →
   envs_app true (Esnoc Enil i P') Δ = Some Δ' →
-  Δ' ⊢ Q → Δ ⊢ (P → Q).
+  (Δ' ⊢ Q) → Δ ⊢ P → Q.
 Proof.
   intros ?? HQ. rewrite envs_app_sound //; simpl. apply impl_intro_l.
   by rewrite right_id {1}(to_persistentP P) always_and_sep_l wand_elim_r.
 Qed.
-Lemma tac_impl_intro_pure Δ P φ Q : ToPure P φ → (φ → Δ ⊢ Q) → Δ ⊢ (P → Q).
+Lemma tac_impl_intro_pure Δ P φ Q : ToPure P φ → (φ → Δ ⊢ Q) → Δ ⊢ P → Q.
 Proof.
   intros. by apply impl_intro_l; rewrite (to_pure P); apply const_elim_l.
 Qed.
 
 Lemma tac_wand_intro Δ Δ' i P Q :
-  envs_app false (Esnoc Enil i P) Δ = Some Δ' → Δ' ⊢ Q → Δ ⊢ (P -★ Q).
+  envs_app false (Esnoc Enil i P) Δ = Some Δ' → (Δ' ⊢ Q) → Δ ⊢ P -★ Q.
 Proof.
   intros ? HQ. rewrite envs_app_sound //; simpl. by rewrite right_id HQ.
 Qed.
 Lemma tac_wand_intro_persistent Δ Δ' i P P' Q :
   ToPersistentP P P' →
   envs_app true (Esnoc Enil i P') Δ = Some Δ' →
-  Δ' ⊢ Q → Δ ⊢ (P -★ Q).
+  (Δ' ⊢ Q) → Δ ⊢ P -★ Q.
 Proof.
   intros. rewrite envs_app_sound //; simpl.
   rewrite right_id. by apply wand_mono.
 Qed.
-Lemma tac_wand_intro_pure Δ P φ Q : ToPure P φ → (φ → Δ ⊢ Q) → Δ ⊢ (P -★ Q).
+Lemma tac_wand_intro_pure Δ P φ Q : ToPure P φ → (φ → Δ ⊢ Q) → Δ ⊢ P -★ Q.
 Proof.
   intros. by apply wand_intro_l; rewrite (to_pure P); apply const_elim_sep_l.
 Qed.
 
-Class ToWand (R P Q : uPred M) := to_wand : R ⊢ (P -★ Q).
+Class ToWand (R P Q : uPred M) := to_wand : R ⊢ P -★ Q.
 Arguments to_wand : clear implicits.
 Global Instance to_wand_wand P Q : ToWand (P -★ Q) P Q.
 Proof. done. Qed.
@@ -483,7 +482,7 @@ Lemma tac_specialize Δ Δ' Δ'' i p j q P1 P2 R Q :
   | false => envs_replace j q false (Esnoc Enil j P2) Δ'
              (* remove [i] and make [j] spatial *)
   end = Some Δ'' →
-  Δ'' ⊢ Q → Δ ⊢ Q.
+  (Δ'' ⊢ Q) → Δ ⊢ Q.
 Proof.
   intros [? ->]%envs_lookup_delete_Some ??? <-. destruct p.
   - rewrite envs_lookup_persistent_sound // envs_simple_replace_sound //; simpl.
@@ -495,7 +494,7 @@ Proof.
 Qed.
 
 Class ToAssert (P : uPred M) (Q : uPred M) (R : uPred M) :=
-  to_assert : (R ★ (P -★ Q)) ⊢ Q.
+  to_assert : R ★ (P -★ Q) ⊢ Q.
 Global Arguments to_assert _ _ _ {_}.
 Lemma to_assert_fallthrough P Q : ToAssert P Q P.
 Proof. by rewrite /ToAssert wand_elim_r. Qed.
@@ -506,7 +505,7 @@ Lemma tac_specialize_assert Δ Δ' Δ1 Δ2' j q lr js R P1 P2 P1' Q :
   ('(Δ1,Δ2) ← envs_split lr js Δ';
     Δ2' ← envs_app false (Esnoc Enil j P2) Δ2;
     Some (Δ1,Δ2')) = Some (Δ1,Δ2') → (* does not preserve position of [j] *)
-  Δ1 ⊢ P1' → Δ2' ⊢ Q → Δ ⊢ Q.
+  (Δ1 ⊢ P1') → (Δ2' ⊢ Q) → Δ ⊢ Q.
 Proof.
   intros [? ->]%envs_lookup_delete_Some ??? HP1 HQ.
   destruct (envs_split _ _ _) as [[? Δ2]|] eqn:?; simplify_eq/=;
@@ -522,7 +521,7 @@ Lemma tac_specialize_pure Δ Δ' j q R P1 P2 φ Q :
   envs_lookup j Δ = Some (q, R) →
   ToWand R P1 P2 → ToPure P1 φ →
   envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ' →
-  φ → Δ' ⊢ Q → Δ ⊢ Q.
+  φ → (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
   intros. rewrite envs_simple_replace_sound //; simpl.
   by rewrite right_id (to_wand R) (to_pure P1) const_equiv // wand_True wand_elim_r.
@@ -532,8 +531,8 @@ Lemma tac_specialize_persistent Δ Δ' Δ'' j q P1 P2 R Q :
   envs_lookup_delete j Δ = Some (q, R, Δ') →
   ToWand R P1 P2 →
   envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ'' →
-  Δ' ⊢ P1 → (PersistentP P1 ∨ PersistentP P2) →
-  Δ'' ⊢ Q → Δ ⊢ Q.
+  (Δ' ⊢ P1) → (PersistentP P1 ∨ PersistentP P2) →
+  (Δ'' ⊢ Q) → Δ ⊢ Q.
 Proof.
   intros [? ->]%envs_lookup_delete_Some ?? HP1 [?|?] <-.
   - rewrite envs_lookup_sound //.
@@ -550,7 +549,7 @@ Qed.
 
 Lemma tac_revert Δ Δ' i p P Q :
   envs_lookup_delete i Δ = Some (p,P,Δ') →
-  Δ' ⊢ (if p then □ P → Q else P -★ Q) → Δ ⊢ Q.
+  (Δ' ⊢ if p then □ P → Q else P -★ Q) → Δ ⊢ Q.
 Proof.
   intros ? HQ. rewrite envs_lookup_delete_sound //; simpl. destruct p.
   - by rewrite HQ -always_and_sep_l impl_elim_r.
@@ -558,7 +557,7 @@ Proof.
 Qed.
 
 Lemma tac_revert_spatial Δ Q :
-  envs_clear_spatial Δ ⊢ (env_fold uPred_wand Q (env_spatial Δ)) → Δ ⊢ Q.
+  (envs_clear_spatial Δ ⊢ env_fold uPred_wand Q (env_spatial Δ)) → Δ ⊢ Q.
 Proof.
   intros HΔ. by rewrite envs_clear_spatial_sound HΔ env_fold_wand wand_elim_l.
 Qed.
@@ -567,7 +566,7 @@ Lemma tac_assert Δ Δ1 Δ2 Δ2' lr js j P Q R :
   ToAssert P Q R →
   envs_split lr js Δ = Some (Δ1,Δ2) →
   envs_app false (Esnoc Enil j P) Δ2 = Some Δ2' →
-  Δ1 ⊢ R → Δ2' ⊢ Q → Δ ⊢ Q.
+  (Δ1 ⊢ R) → (Δ2' ⊢ Q) → Δ ⊢ Q.
 Proof.
   intros ??? HP HQ. rewrite envs_split_sound //.
   rewrite (envs_app_sound Δ2) //; simpl.
@@ -576,7 +575,7 @@ Qed.
 
 Lemma tac_assert_persistent Δ Δ' j P Q :
   envs_app true (Esnoc Enil j P) Δ = Some Δ' →
-  Δ ⊢ P → PersistentP P → Δ' ⊢ Q → Δ ⊢ Q.
+  (Δ ⊢ P) → PersistentP P → (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
   intros ? HP ??.
   rewrite -(idemp uPred_and Δ) {1}HP envs_app_sound //; simpl.
@@ -587,7 +586,7 @@ Qed.
 not as [H : True -★ Q]. The class [ToPosedProof] is used to strip off the
 [True]. Note that [to_posed_proof_True] is declared using a [Hint Extern] to
 make sure it is not used while posing [lem : ?P ⊢ Q] with [?P] an evar. *)
-Class ToPosedProof (P1 P2 R : uPred M) := to_pose_proof : P1 ⊢ P2 → True ⊢ R.
+Class ToPosedProof (P1 P2 R : uPred M) := to_pose_proof : (P1 ⊢ P2) → True ⊢ R.
 Arguments to_pose_proof : clear implicits.
 Instance to_posed_proof_True P : ToPosedProof True P P.
 Proof. by rewrite /ToPosedProof. Qed.
@@ -595,8 +594,8 @@ Global Instance to_posed_proof_wand P Q : ToPosedProof P Q (P -★ Q).
 Proof. rewrite /ToPosedProof. apply entails_wand. Qed.
 
 Lemma tac_pose_proof Δ Δ' j P1 P2 R Q :
-  P1 ⊢ P2 → ToPosedProof P1 P2 R → envs_app true (Esnoc Enil j R) Δ = Some Δ' →
-  Δ' ⊢ Q → Δ ⊢ Q.
+  (P1 ⊢ P2) → ToPosedProof P1 P2 R → envs_app true (Esnoc Enil j R) Δ = Some Δ' →
+  (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
   intros HP ?? <-. rewrite envs_app_sound //; simpl.
   by rewrite right_id -(to_pose_proof P1 P2 R) // always_const wand_True.
@@ -605,7 +604,7 @@ Qed.
 Lemma tac_pose_proof_hyp Δ Δ' Δ'' i p j P Q :
   envs_lookup_delete i Δ = Some (p, P, Δ') →
   envs_app p (Esnoc Enil j P) (if p then Δ else Δ') = Some Δ'' →
-  Δ'' ⊢ Q → Δ ⊢ Q.
+  (Δ'' ⊢ Q) → Δ ⊢ Q.
 Proof.
   intros [? ->]%envs_lookup_delete_Some ? <-. destruct p.
   - rewrite envs_lookup_persistent_sound // envs_app_sound //; simpl.
@@ -616,7 +615,7 @@ Qed.
 
 Lemma tac_apply Δ Δ' i p R P1 P2 :
   envs_lookup_delete i Δ = Some (p, R, Δ') → ToWand R P1 P2 →
-  Δ' ⊢ P1 → Δ ⊢ P2.
+  (Δ' ⊢ P1) → Δ ⊢ P2.
 Proof.
   intros ?? HP1. rewrite envs_lookup_delete_sound' //.
   by rewrite (to_wand R) HP1 wand_elim_l.
@@ -626,10 +625,10 @@ Qed.
 Lemma tac_rewrite Δ i p Pxy (lr : bool) Q :
   envs_lookup i Δ = Some (p, Pxy) →
   ∀ {A : cofeT} (x y : A) (Φ : A → uPred M),
-    Pxy ⊢ (x ≡ y) →
-    Q ⊣⊢ Φ (if lr then y else x) →
+    (Pxy ⊢ x ≡ y) →
+    (Q ⊣⊢ Φ (if lr then y else x)) →
     (∀ n, Proper (dist n ==> dist n) Φ) →
-    Δ ⊢ Φ (if lr then x else y) → Δ ⊢ Q.
+    (Δ ⊢ Φ (if lr then x else y)) → Δ ⊢ Q.
 Proof.
   intros ? A x y ? HPxy -> ?; apply eq_rewrite; auto.
   rewrite {1}envs_lookup_sound' //; rewrite sep_elim_l HPxy.
@@ -640,11 +639,11 @@ Lemma tac_rewrite_in Δ i p Pxy j q P (lr : bool) Q :
   envs_lookup i Δ = Some (p, Pxy) →
   envs_lookup j Δ = Some (q, P) →
   ∀ {A : cofeT} Δ' x y (Φ : A → uPred M),
-    Pxy ⊢ (x ≡ y) →
-    P ⊣⊢ Φ (if lr then y else x) →
+    (Pxy ⊢ x ≡ y) →
+    (P ⊣⊢ Φ (if lr then y else x)) →
     (∀ n, Proper (dist n ==> dist n) Φ) →
     envs_simple_replace j q (Esnoc Enil j (Φ (if lr then x else y))) Δ = Some Δ' →
-    Δ' ⊢ Q → Δ ⊢ Q.
+    (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
   intros ?? A Δ' x y Φ HPxy HP ?? <-.
   rewrite -(idemp uPred_and Δ) {2}(envs_lookup_sound' _ i) //.
@@ -657,7 +656,7 @@ Proof.
 Qed.
 
 (** * Conjunction splitting *)
-Class AndSplit (P Q1 Q2 : uPred M) := and_split : (Q1 ∧ Q2) ⊢ P.
+Class AndSplit (P Q1 Q2 : uPred M) := and_split : Q1 ∧ Q2 ⊢ P.
 Arguments and_split : clear implicits.
 
 Global Instance and_split_and P1 P2 : AndSplit (P1 ∧ P2) P1 P2.
@@ -669,11 +668,11 @@ Global Instance and_split_sep_persistent_r P1 P2 :
   PersistentP P2 → AndSplit (P1 ★ P2) P1 P2.
 Proof. intros. by rewrite /AndSplit always_and_sep_r. Qed.
 
-Lemma tac_and_split Δ P Q1 Q2 : AndSplit P Q1 Q2 → Δ ⊢ Q1 → Δ ⊢ Q2 → Δ ⊢ P.
+Lemma tac_and_split Δ P Q1 Q2 : AndSplit P Q1 Q2 → (Δ ⊢ Q1) → (Δ ⊢ Q2) → Δ ⊢ P.
 Proof. intros. rewrite -(and_split P). by apply and_intro. Qed.
 
 (** * Separating conjunction splitting *)
-Class SepSplit (P Q1 Q2 : uPred M) := sep_split : (Q1 ★ Q2) ⊢ P.
+Class SepSplit (P Q1 Q2 : uPred M) := sep_split : Q1 ★ Q2 ⊢ P.
 Arguments sep_split : clear implicits.
 
 Global Instance sep_split_sep P1 P2 : SepSplit (P1 ★ P2) P1 P2 | 100.
@@ -699,7 +698,7 @@ Qed.
 Lemma tac_sep_split Δ Δ1 Δ2 lr js P Q1 Q2 :
   SepSplit P Q1 Q2 →
   envs_split lr js Δ = Some (Δ1,Δ2) →
-  Δ1 ⊢ Q1 → Δ2 ⊢ Q2 → Δ ⊢ P.
+  (Δ1 ⊢ Q1) → (Δ2 ⊢ Q2) → Δ ⊢ P.
 Proof.
   intros. rewrite envs_split_sound // -(sep_split P). by apply sep_mono.
 Qed.
@@ -711,7 +710,7 @@ Lemma tac_combine Δ1 Δ2 Δ3 Δ4 i1 p P1 i2 q P2 j P Q :
   SepSplit P P1 P2 →
   envs_app (p && q) (Esnoc Enil j P)
     (if q then (if p then Δ1 else Δ2) else Δ3) = Some Δ4 →
-  Δ4 ⊢ Q → Δ1 ⊢ Q.
+  (Δ4 ⊢ Q) → Δ1 ⊢ Q.
 Proof.
   intros [? ->]%envs_lookup_delete_Some [? ->]%envs_lookup_delete_Some ?? <-.
   destruct p.
@@ -748,9 +747,6 @@ Global Instance op_destruct_Some {A : cmraT} (a : A) b1 b2 :
   OpDestruct a b1 b2 → OpDestruct (Some a) (Some b1) (Some b2).
 Proof. by constructor. Qed.
 
-Lemma sep_destruct_spatial p P Q1 Q2 : P ⊢ (Q1 ★ Q2) → SepDestruct p P Q1 Q2.
-Proof. rewrite /SepDestruct=> ->. by rewrite always_if_sep. Qed.
-
 Global Instance sep_destruct_sep p P Q : SepDestruct p (P ★ Q) P Q.
 Proof. rewrite /SepDestruct. by rewrite always_if_sep. Qed.
 Global Instance sep_destruct_ownM p (a b1 b2 : M) :
@@ -793,7 +789,7 @@ Qed.
 Lemma tac_sep_destruct Δ Δ' i p j1 j2 P P1 P2 Q :
   envs_lookup i Δ = Some (p, P) → SepDestruct p P P1 P2 →
   envs_simple_replace i p (Esnoc (Esnoc Enil j1 P1) j2 P2) Δ = Some Δ' →
-  Δ' ⊢ Q → Δ ⊢ Q.
+  (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
   intros. rewrite envs_simple_replace_sound //; simpl.
   by rewrite (sep_destruct p P) right_id (comm uPred_sep P1) wand_elim_r.
@@ -803,7 +799,7 @@ Qed.
 (** The [option] is to account for formulas that can be framed entirely, so
 we do not end up with [True]s everywhere. *)
 Class Frame (R P : uPred M) (mQ : option (uPred M)) :=
-  frame : (R ★ from_option id True mQ) ⊢ P.
+  frame : R ★ from_option id True mQ ⊢ P.
 Arguments frame : clear implicits.
 
 Global Instance frame_here R : Frame R R None.
@@ -862,17 +858,17 @@ Proof.
 Qed.
 
 (** * Disjunction *)
-Class OrSplit (P Q1 Q2 : uPred M) := or_split : (Q1 ∨ Q2) ⊢ P.
+Class OrSplit (P Q1 Q2 : uPred M) := or_split : Q1 ∨ Q2 ⊢ P.
 Arguments or_split : clear implicits.
 Global Instance or_split_or P1 P2 : OrSplit (P1 ∨ P2) P1 P2.
 Proof. done. Qed.
 
-Lemma tac_or_l Δ P Q1 Q2 : OrSplit P Q1 Q2 → Δ ⊢ Q1 → Δ ⊢ P.
+Lemma tac_or_l Δ P Q1 Q2 : OrSplit P Q1 Q2 → (Δ ⊢ Q1) → Δ ⊢ P.
 Proof. intros. rewrite -(or_split P). by apply or_intro_l'. Qed.
-Lemma tac_or_r Δ P Q1 Q2 : OrSplit P Q1 Q2 → Δ ⊢ Q2 → Δ ⊢ P.
+Lemma tac_or_r Δ P Q1 Q2 : OrSplit P Q1 Q2 → (Δ ⊢ Q2) → Δ ⊢ P.
 Proof. intros. rewrite -(or_split P). by apply or_intro_r'. Qed.
 
-Class OrDestruct P Q1 Q2 := or_destruct : P ⊢ (Q1 ∨ Q2).
+Class OrDestruct P Q1 Q2 := or_destruct : P ⊢ Q1 ∨ Q2.
 Arguments or_destruct : clear implicits.
 Global Instance or_destruct_or P Q : OrDestruct (P ∨ Q) P Q.
 Proof. done. Qed.
@@ -884,7 +880,7 @@ Lemma tac_or_destruct Δ Δ1 Δ2 i p j1 j2 P P1 P2 Q :
   envs_lookup i Δ = Some (p, P) → OrDestruct P P1 P2 →
   envs_simple_replace i p (Esnoc Enil j1 P1) Δ = Some Δ1 →
   envs_simple_replace i p (Esnoc Enil j2 P2) Δ = Some Δ2 →
-  Δ1 ⊢ Q → Δ2 ⊢ Q → Δ ⊢ Q.
+  (Δ1 ⊢ Q) → (Δ2 ⊢ Q) → Δ ⊢ Q.
 Proof.
   intros ???? HP1 HP2. rewrite envs_lookup_sound //.
   rewrite (or_destruct P) always_if_or sep_or_r; apply or_elim.
@@ -895,7 +891,7 @@ Proof.
 Qed.
 
 (** * Forall *)
-Lemma tac_forall_intro {A} Δ (Φ : A → uPred M) : (∀ a, Δ ⊢ Φ a) → Δ ⊢ (∀ a, Φ a).
+Lemma tac_forall_intro {A} Δ (Φ : A → uPred M) : (∀ a, Δ ⊢ Φ a) → Δ ⊢ ∀ a, Φ a.
 Proof. apply forall_intro. Qed.
 
 Class ForallSpecialize {As} (xs : hlist As)
@@ -913,14 +909,14 @@ Proof. rewrite /ForallSpecialize /= => <-. by rewrite (forall_elim x). Qed.
 Lemma tac_forall_specialize {As} Δ Δ' i p P (Φ : himpl As (uPred M)) Q xs :
   envs_lookup i Δ = Some (p, P) → ForallSpecialize xs P Φ →
   envs_simple_replace i p (Esnoc Enil i (happly Φ xs)) Δ = Some Δ' →
-  Δ' ⊢ Q → Δ ⊢ Q.
+  (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
   intros. rewrite envs_simple_replace_sound //; simpl.
   by rewrite right_id (forall_specialize _ P) wand_elim_r.
 Qed.
 
 Lemma tac_forall_revert {A} Δ (Φ : A → uPred M) :
-  Δ ⊢ (∀ a, Φ a) → (∀ a, Δ ⊢ Φ a).
+  (Δ ⊢ ∀ a, Φ a) → ∀ a, Δ ⊢ Φ a.
 Proof. intros HΔ a. by rewrite HΔ (forall_elim a). Qed.
 
 (** * Existential *)
@@ -935,7 +931,7 @@ Lemma tac_exist {A} Δ P (Φ : A → uPred M) :
 Proof. intros ? [a ?]. rewrite -(exist_split P). eauto using exist_intro'. Qed.
 
 Class ExistDestruct {A} (P : uPred M) (Φ : A → uPred M) :=
-  exist_destruct : P ⊢ (∃ x, Φ x).
+  exist_destruct : P ⊢ ∃ x, Φ x.
 Arguments exist_destruct {_} _ _ {_}.
 Global Instance exist_destruct_exist {A} (Φ : A → uPred M) :
   ExistDestruct (∃ a, Φ a) Φ.
@@ -947,7 +943,7 @@ Proof. rewrite /ExistDestruct=> HP ?. by rewrite HP later_exist. Qed.
 Lemma tac_exist_destruct {A} Δ i p j P (Φ : A → uPred M) Q :
   envs_lookup i Δ = Some (p, P) → ExistDestruct P Φ →
   (∀ a, ∃ Δ',
-    envs_simple_replace i p (Esnoc Enil j (Φ a)) Δ = Some Δ' ∧ Δ' ⊢ Q) →
+    envs_simple_replace i p (Esnoc Enil j (Φ a)) Δ = Some Δ' ∧ (Δ' ⊢ Q)) →
   Δ ⊢ Q.
 Proof.
   intros ?? HΦ. rewrite envs_lookup_sound //.
diff --git a/proofmode/invariants.v b/proofmode/invariants.v
index 9758f82bcd7742db832d361bd217cc4469deab40..fbb6478ec5880198823c56c4bddf31b8815ee6e7 100644
--- a/proofmode/invariants.v
+++ b/proofmode/invariants.v
@@ -10,9 +10,9 @@ Implicit Types P Q R : iProp Λ Σ.
 
 Lemma tac_inv_fsa {A} (fsa : FSA Λ Σ A) fsaV Δ Δ' E N i P Q Φ :
   FSASplit Q E fsa fsaV Φ →
-  fsaV → nclose N ⊆ E → of_envs Δ ⊢ inv N P →
+  fsaV → nclose N ⊆ E → (of_envs Δ ⊢ inv N P) →
   envs_app false (Esnoc Enil i (▷ P)) Δ = Some Δ' →
-  Δ' ⊢ fsa (E ∖ nclose N) (λ a, ▷ P ★ Φ a) → Δ ⊢ Q.
+  (Δ' ⊢ fsa (E ∖ nclose N) (λ a, ▷ P ★ Φ a)) → Δ ⊢ Q.
 Proof.
   intros ????? HΔ'. rewrite -(fsa_split Q) -(inv_fsa fsa _ _ P) //.
   rewrite // -always_and_sep_l. apply and_intro; first done.
@@ -21,9 +21,9 @@ Qed.
 
 Lemma tac_inv_fsa_timeless {A} (fsa : FSA Λ Σ A) fsaV Δ Δ' E N i P Q Φ :
   FSASplit Q E fsa fsaV Φ →
-  fsaV → nclose N ⊆ E → of_envs Δ ⊢ inv N P → TimelessP P →
+  fsaV → nclose N ⊆ E → (of_envs Δ ⊢ inv N P) → TimelessP P →
   envs_app false (Esnoc Enil i P) Δ = Some Δ' →
-  Δ' ⊢ fsa (E ∖ nclose N) (λ a, P ★ Φ a) → Δ ⊢ Q.
+  (Δ' ⊢ fsa (E ∖ nclose N) (λ a, P ★ Φ a)) → Δ ⊢ Q.
 Proof.
   intros ?????? HΔ'. rewrite -(fsa_split Q) -(inv_fsa fsa _ _ P) //.
   rewrite // -always_and_sep_l. apply and_intro, wand_intro_l; first done.
diff --git a/proofmode/pviewshifts.v b/proofmode/pviewshifts.v
index 67f2bc7dbb7273abab44157a711c320a58ed3fa6..f49d3f7a2401e2fa28d0b88c42ee897c1acb4b26 100644
--- a/proofmode/pviewshifts.v
+++ b/proofmode/pviewshifts.v
@@ -49,7 +49,7 @@ Proof.
   by rewrite /ToAssert pvs_frame_r wand_elim_r -(fsa_split Q) fsa_pvs_fsa.
 Qed.
 
-Lemma tac_pvs_intro Δ E1 E2 Q : E1 = E2 → Δ ⊢ Q → Δ ⊢ |={E1,E2}=> Q.
+Lemma tac_pvs_intro Δ E1 E2 Q : E1 = E2 → (Δ ⊢ Q) → Δ ⊢ |={E1,E2}=> Q.
 Proof. intros -> ->. apply pvs_intro. Qed.
 
 Lemma tac_pvs_elim Δ Δ' E1 E2 E3 i p P' E1' E2' P Q :
@@ -69,7 +69,7 @@ Lemma tac_pvs_elim_fsa {A} (fsa : FSA Λ Σ A) fsaV Δ Δ' E i p P' P Q Φ :
   envs_lookup i Δ = Some (p, P') → P' = (|={E}=> P)%I →
   FSASplit Q E fsa fsaV Φ →
   envs_replace i p false (Esnoc Enil i P) Δ = Some Δ' →
-  Δ' ⊢ fsa E Φ → Δ ⊢ Q.
+  (Δ' ⊢ fsa E Φ) → Δ ⊢ Q.
 Proof.
   intros ? -> ??. rewrite -(fsa_split Q) -fsa_pvs_fsa.
   eapply tac_pvs_elim; set_solver.
@@ -89,7 +89,7 @@ Lemma tac_pvs_timeless_fsa {A} (fsa : FSA Λ Σ A) fsaV Δ Δ' E i p P Q Φ :
   FSASplit Q E fsa fsaV Φ →
   envs_lookup i Δ = Some (p, ▷ P)%I → TimelessP P →
   envs_simple_replace i p (Esnoc Enil i P) Δ = Some Δ' →
-  Δ' ⊢ fsa E Φ → Δ ⊢ Q.
+  (Δ' ⊢ fsa E Φ) → Δ ⊢ Q.
 Proof.
   intros ????. rewrite -(fsa_split Q) -fsa_pvs_fsa.
   eauto using tac_pvs_timeless.
diff --git a/proofmode/sts.v b/proofmode/sts.v
index d234c5dec6a6aa4c8bab2d9ec89b812e444f4b36..a3b588195db07ae5709793a209167e5b40195e86 100644
--- a/proofmode/sts.v
+++ b/proofmode/sts.v
@@ -11,11 +11,11 @@ Lemma tac_sts_fsa {A} (fsa : FSA Λ _ A) fsaV Δ E N i γ S T Q Φ :
   FSASplit Q E fsa fsaV Φ →
   fsaV →
   envs_lookup i Δ = Some (false, sts_ownS γ S T) →
-  of_envs Δ ⊢ sts_ctx γ N φ → nclose N ⊆ E →
+  (of_envs Δ ⊢ sts_ctx γ N φ) → nclose N ⊆ E →
   (∀ s, s ∈ S → ∃ Δ',
     envs_simple_replace i false (Esnoc Enil i (▷ φ s)) Δ = Some Δ' ∧
-    Δ' ⊢ fsa (E ∖ nclose N) (λ a, ∃ s' T',
-      ■ sts.steps (s, T) (s', T') ★ ▷ φ s' ★ (sts_own γ s' T' -★ Φ a))) →
+    (Δ' ⊢ fsa (E ∖ nclose N) (λ a, ∃ s' T',
+      ■ sts.steps (s, T) (s', T') ★ ▷ φ s' ★ (sts_own γ s' T' -★ Φ a)))) →
   Δ ⊢ Q.
 Proof.
   intros ????? HΔ'. rewrite -(fsa_split Q) -(sts_fsaS φ fsa) //.
diff --git a/tests/barrier_client.v b/tests/barrier_client.v
index ca07236f2934682a3f01dc886718d89070dad283..e1699c43ea1e5ee4acb60c6df01f3f612759d36b 100644
--- a/tests/barrier_client.v
+++ b/tests/barrier_client.v
@@ -27,7 +27,7 @@ Section client.
   Qed.
 
   Lemma worker_safe q (n : Z) (b y : loc) :
-    (heap_ctx heapN ★ recv heapN N b (y_inv q y))
+    heap_ctx heapN ★ recv heapN N b (y_inv q y)
     ⊢ WP worker n #b #y {{ _, True }}.
   Proof.
     iIntros "[#Hh Hrecv]". wp_lam. wp_let.
diff --git a/tests/joining_existentials.v b/tests/joining_existentials.v
index 02888a70c567ab648c4a2bf6d4eb910cf8549d67..c8d19f894b0c4dca58dbca494c1f23f284eebf04 100644
--- a/tests/joining_existentials.v
+++ b/tests/joining_existentials.v
@@ -20,7 +20,7 @@ Definition barrier_res γ (Φ : X → iProp) : iProp :=
   (∃ x, one_shot_own γ x ★ Φ x)%I.
 
 Lemma worker_spec e γ l (Φ Ψ : X → iProp) :
-  (recv heapN N l (barrier_res γ Φ) ★ ∀ x, {{ Φ x }} e {{ _, Ψ x }})
+  recv heapN N l (barrier_res γ Φ) ★ (∀ x, {{ Φ x }} e {{ _, Ψ x }})
   ⊢ WP wait #l ;; e {{ _, barrier_res γ Ψ }}.
 Proof.
   iIntros "[Hl #He]". wp_apply wait_spec; iFrame "Hl".
@@ -33,13 +33,13 @@ Context (P : iProp) (Φ Φ1 Φ2 Ψ Ψ1 Ψ2 : X -n> iProp).
 Context {Φ_split : ∀ x, Φ x ⊢ (Φ1 x ★ Φ2 x)}.
 Context {Ψ_join  : ∀ x, (Ψ1 x ★ Ψ2 x) ⊢ Ψ x}.
 
-Lemma P_res_split γ : barrier_res γ Φ ⊢ (barrier_res γ Φ1 ★ barrier_res γ Φ2).
+Lemma P_res_split γ : barrier_res γ Φ ⊢ barrier_res γ Φ1 ★ barrier_res γ Φ2.
 Proof.
   iIntros "Hγ"; iDestruct "Hγ" as {x} "[#Hγ Hx]".
   iDestruct (Φ_split with "Hx") as "[H1 H2]". by iSplitL "H1"; iExists x; iSplit.
 Qed.
 
-Lemma Q_res_join γ : (barrier_res γ Ψ1 ★ barrier_res γ Ψ2) ⊢ ▷ barrier_res γ Ψ.
+Lemma Q_res_join γ : barrier_res γ Ψ1 ★ barrier_res γ Ψ2 ⊢ ▷ barrier_res γ Ψ.
 Proof.
   iIntros "[Hγ Hγ']";
   iDestruct "Hγ" as {x} "[#Hγ Hx]"; iDestruct "Hγ'" as {x'} "[#Hγ' Hx']".
@@ -50,10 +50,10 @@ Qed.
 
 Lemma client_spec_new (eM eW1 eW2 : expr []) (eM' eW1' eW2' : expr ("b" :b: [])) :
   heapN ⊥ N → eM' = wexpr' eM → eW1' = wexpr' eW1 → eW2' = wexpr' eW2 →
-  (heap_ctx heapN ★ P
+  heap_ctx heapN ★ P
   ★ {{ P }} eM {{ _, ∃ x, Φ x }}
   ★ (∀ x, {{ Φ1 x }} eW1 {{ _, Ψ1 x }})
-  ★ (∀ x, {{ Φ2 x }} eW2 {{ _, Ψ2 x }}))
+  ★ (∀ x, {{ Φ2 x }} eW2 {{ _, Ψ2 x }})
   ⊢ WP client eM' eW1' eW2' {{ _, ∃ γ, barrier_res γ Ψ }}.
 Proof.
   iIntros {HN -> -> ->} "/= (#Hh&HP&#He&#He1&#He2)"; rewrite /client.
diff --git a/tests/one_shot.v b/tests/one_shot.v
index 22fe7d867ce663368daba66129693d391444290a..2d0857324777b63f03274710ca8f9f3bd82cd5c6 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -37,7 +37,7 @@ Definition one_shot_inv (γ : gname) (l : loc) : iProp :=
   ∃ n : Z, l ↦ InjRV #n ★ own γ (Shot (DecAgree n)))%I.
 
 Lemma wp_one_shot (Φ : val → iProp) :
-  (heap_ctx heapN ★ ∀ f1 f2 : val,
+  heap_ctx heapN ★ (∀ f1 f2 : val,
     (∀ n : Z, □ WP f1 #n {{ w, w = #true ∨ w = #false }}) ★
     □ WP f2 #() {{ g, □ WP g #() {{ _, True }} }} -★ Φ (f1,f2)%V)
   ⊢ WP one_shot_example #() {{ Φ }}.
diff --git a/tests/proofmode.v b/tests/proofmode.v
index c244c1078f07f9670ea2a2aab134cd20eeb74de9..02e9a825ccd5dafcd1b274eeb287ab102798c142 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -2,7 +2,7 @@ From iris.proofmode Require Import tactics.
 From iris.proofmode Require Import pviewshifts invariants.
 
 Lemma demo_0 {M : ucmraT} (P Q : uPred M) :
-  □ (P ∨ Q) ⊢ ((∀ x, x = 0 ∨ x = 1) → (Q ∨ P)).
+  □ (P ∨ Q) ⊢ (∀ x, x = 0 ∨ x = 1) → (Q ∨ P).
 Proof.
   iIntros "#H #H2".
   (* should remove the disjunction "H" *)
@@ -12,13 +12,13 @@ Proof.
 Qed.
 
 Lemma demo_1 (M : ucmraT) (P1 P2 P3 : nat → uPred M) :
-  True ⊢ (∀ (x y : nat) a b,
+  True ⊢ ∀ (x y : nat) a b,
     x ≡ y →
     □ (uPred_ownM (a ⋅ b) -★
     (∃ y1 y2 c, P1 ((x + y1) + y2) ∧ True ∧ □ uPred_ownM c) -★
     □ ▷ (∀ z, P2 z ∨ True → P2 z) -★
     ▷ (∀ n m : nat, P1 n → □ ((True ∧ P2 n) → □ (n = n ↔ P3 n))) -★
-    ▷ (x = 0) ∨ ∃ x z, ▷ P3 (x + z) ★ uPred_ownM b ★ uPred_ownM (core b))).
+    ▷ (x = 0) ∨ ∃ x z, ▷ P3 (x + z) ★ uPred_ownM b ★ uPred_ownM (core b)).
 Proof.
   iIntros {i [|j] a b ?} "! [Ha Hb] H1 #H2 H3"; setoid_subst.
   { iLeft. by iNext. }
@@ -37,9 +37,9 @@ Proof.
 Qed.
 
 Lemma demo_2 (M : ucmraT) (P1 P2 P3 P4 Q : uPred M) (P5 : nat → uPredC M):
-    (P2 ★ (P3 ★ Q) ★ True ★ P1 ★ P2 ★ (P4 ★ (∃ x:nat, P5 x ∨ P3)) ★ True)
-  ⊢ (P1 -★ (True ★ True) -★ (((P2 ∧ False ∨ P2 ∧ 0 = 0) ★ P3) ★ Q ★ P1 ★ True) ∧
-     (P2 ∨ False) ∧ (False → P5 0)).
+    P2 ★ (P3 ★ Q) ★ True ★ P1 ★ P2 ★ (P4 ★ (∃ x:nat, P5 x ∨ P3)) ★ True
+  ⊢ P1 -★ (True ★ True) -★ (((P2 ∧ False ∨ P2 ∧ 0 = 0) ★ P3) ★ Q ★ P1 ★ True) ∧
+     (P2 ∨ False) ∧ (False → P5 0).
 Proof.
   (* Intro-patterns do something :) *)
   iIntros "[H2 ([H3 HQ]&?&H1&H2'&foo&_)] ? [??]".
@@ -54,7 +54,7 @@ Proof.
 Qed.
 
 Lemma demo_3 (M : ucmraT) (P1 P2 P3 : uPred M) :
-  (P1 ★ P2 ★ P3) ⊢ (▷ P1 ★ ▷ (P2 ★ ∃ x, (P3 ∧ x = 0) ∨ P3)).
+  P1 ★ P2 ★ P3 ⊢ ▷ P1 ★ ▷ (P2 ★ ∃ x, (P3 ∧ x = 0) ∨ P3).
 Proof. iIntros "($ & $ & H)". iFrame "H". iNext. by iExists 0. Qed.
 
 Definition foo {M} (P : uPred M) := (P → P)%I.
@@ -73,8 +73,8 @@ Proof.
 Qed.
 
 Lemma demo_6 (M : ucmraT) (P Q : uPred M) :
-  True ⊢ (∀ x y z : nat,
-    x = plus 0 x → y = 0 → z = 0 → P → □ Q → foo (x ≡ x)).
+  True ⊢ ∀ x y z : nat,
+    x = plus 0 x → y = 0 → z = 0 → P → □ Q → foo (x ≡ x).
 Proof.
   iIntros {a} "*".
   iIntros "#Hfoo **".
@@ -97,7 +97,7 @@ Section iris.
 
   Lemma demo_8 N E P Q R :
     nclose N ⊆ E →
-    (True -★ P -★ inv N Q -★ True -★ R) ⊢ (P -★ ▷ Q -★ |={E}=> R).
+    (True -★ P -★ inv N Q -★ True -★ R) ⊢ P -★ ▷ Q -★ |={E}=> R.
   Proof.
     iIntros {?} "H HP HQ".
     iApply ("H" with "[#] HP =>[HQ] =>").