diff --git a/theories/lifetime/at_borrow.v b/theories/lifetime/at_borrow.v
index 01e19df60714cbab72b5e43de6d7615cae58cf23..3ce37b766398dbf5a2e57ebdd4cbd0d52df5d908 100644
--- a/theories/lifetime/at_borrow.v
+++ b/theories/lifetime/at_borrow.v
@@ -9,8 +9,8 @@ Definition at_bor `{invG Σ, lftG Σ} κ N (P : iProp Σ) :=
   (∃ i, &{κ,i}P ∗
     (⌜N ⊥ lftN⌝ ∗ inv N (idx_bor_own 1 i) ∨
      ⌜N = lftN⌝ ∗ inv N (∃ q, idx_bor_own q i)))%I.
-Notation "&at{ κ , N } P" := (at_bor κ N P)
-  (format "&at{ κ , N }  P", at level 20, right associativity) : uPred_scope.
+Notation "&at{ κ , N }" := (at_bor κ N)
+  (format "&at{ κ , N }", at level 20, right associativity) : uPred_scope.
 
 Section atomic_bors.
   Context `{invG Σ, lftG Σ} (P : iProp Σ) (N : namespace).
@@ -31,9 +31,9 @@ Section atomic_bors.
   Global Instance at_bor_persistent : PersistentP (&at{κ, N} P) := _.
 
   Lemma bor_share E κ :
-    ↑lftN ⊆ E → N ⊥ lftN → &{κ}P ={E}=∗ &at{κ, N}P.
+    N ⊥ lftN → &{κ}P ={E}=∗ &at{κ, N}P.
   Proof.
-    iIntros (? HN) "HP". rewrite bor_unfold_idx. iDestruct "HP" as (i) "(#?&Hown)".
+    iIntros (HN) "HP". rewrite bor_unfold_idx. iDestruct "HP" as (i) "(#?&Hown)".
     iExists i. iFrame "#".
     iLeft. iSplitR. done. by iMod (inv_alloc with "[Hown]") as "$"; auto.
   Qed.
diff --git a/theories/lifetime/frac_borrow.v b/theories/lifetime/frac_borrow.v
index 6ff33ee6c813f5d4a09c9ad48e92f85b0350809b..eb8513025e581cc45efd8ad4392c54cef5afe17f 100644
--- a/theories/lifetime/frac_borrow.v
+++ b/theories/lifetime/frac_borrow.v
@@ -8,10 +8,10 @@ Set Default Proof Using "Type".
 Class frac_borG Σ := frac_borG_inG :> inG Σ fracR.
 
 Definition frac_bor `{invG Σ, lftG Σ, frac_borG Σ} κ (φ : Qp → iProp Σ) :=
-  (∃ γ κ', κ ⊑ κ' ∗ &at{κ',lftN} ∃ q, φ q ∗ own γ q ∗
-                       (⌜q = 1%Qp⌝ ∨ ∃ q', ⌜(q + q' = 1)%Qp⌝ ∗ q'.[κ']))%I.
-Notation "&frac{ κ } P" := (frac_bor κ P)
-  (format "&frac{ κ }  P", at level 20, right associativity) : uPred_scope.
+  (∃ γ κ', κ ⊑ κ' ∗ &at{κ',lftN} (∃ q, φ q ∗ own γ q ∗
+                       (⌜q = 1%Qp⌝ ∨ ∃ q', ⌜(q + q' = 1)%Qp⌝ ∗ q'.[κ'])))%I.
+Notation "&frac{ κ }" := (frac_bor κ)
+  (format "&frac{ κ }", at level 20, right associativity) : uPred_scope.
 
 Section frac_bor.
   Context `{invG Σ, lftG Σ, frac_borG Σ} (φ : Qp → iProp Σ).
diff --git a/theories/lifetime/lifetime.v b/theories/lifetime/lifetime.v
index 06cd7e40bc8bdc3985c05e18b0a1567c18167fe4..82200abc1323647c82c559628d7eb1e0cab51bef 100644
--- a/theories/lifetime/lifetime.v
+++ b/theories/lifetime/lifetime.v
@@ -75,7 +75,7 @@ Qed.
 
 Lemma bor_exists {A} (Φ : A → iProp Σ) `{!Inhabited A} E κ :
   ↑lftN ⊆ E →
-  lft_ctx -∗ &{κ}(∃ x, Φ x) ={E}=∗ ∃ x, &{κ}Φ x.
+  lft_ctx -∗ &{κ}(∃ x, Φ x) ={E}=∗ ∃ x, &{κ}(Φ x).
 Proof.
   iIntros (?) "#LFT Hb".
   iMod (bor_acc_atomic_cons with "LFT Hb") as "[H|[H† >_]]"; first done.
@@ -168,7 +168,7 @@ Qed.
 
 Lemma bor_unnest E κ κ' P :
   ↑lftN ⊆ E →
-  lft_ctx -∗ &{κ'} &{κ} P ={E}▷=∗ &{κ ⊓ κ'} P.
+  lft_ctx -∗ &{κ'} (&{κ} P) ={E}▷=∗ &{κ ⊓ κ'} P.
 Proof.
   iIntros (?) "#LFT Hbor".
   rewrite ->(bor_unfold_idx _ P).
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index 58d85fb187a1d39928522e449a7de0945330c832..e370a2b7d9e263d299fa318cf4a02e3dcc7453d6 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -39,10 +39,10 @@ Module Type lifetime_sig.
       (format "q .[ κ ]", at level 0) : uPred_scope.
   Notation "[† κ ]" := (lft_dead κ) (format "[† κ ]"): uPred_scope.
 
-  Notation "&{ κ } P" := (bor κ P)
-    (format "&{ κ }  P", at level 20, right associativity) : uPred_scope.
-  Notation "&{ κ , i } P" := (idx_bor κ i P)
-    (format "&{ κ , i }  P", at level 20, right associativity) : uPred_scope.
+  Notation "&{ κ }" := (bor κ)
+    (format "&{ κ }", at level 20, right associativity) : uPred_scope.
+  Notation "&{ κ , i }" := (idx_bor κ i)
+    (format "&{ κ , i }", at level 20, right associativity) : uPred_scope.
 
   Infix "⊑" := lft_incl (at level 70) : uPred_scope.
   Infix "⊓" := lft_intersect (at level 40) : C_scope.
@@ -115,7 +115,7 @@ Module Type lifetime_sig.
   Parameter idx_bor_iff : ∀ κ i P P', ▷ □ (P ↔ P') -∗ &{κ,i}P -∗ &{κ,i}P'.
 
   Parameter idx_bor_unnest : ∀ E κ κ' i P,
-    ↑lftN ⊆ E → lft_ctx -∗ &{κ,i} P -∗ &{κ'} idx_bor_own 1 i ={E}=∗ &{κ ⊓ κ'} P.
+    ↑lftN ⊆ E → lft_ctx -∗ &{κ,i} P -∗ &{κ'}(idx_bor_own 1 i) ={E}=∗ &{κ ⊓ κ'} P.
 
   Parameter idx_bor_acc : ∀ E q κ i P, ↑lftN ⊆ E →
     lft_ctx -∗ &{κ,i}P -∗ idx_bor_own 1 i -∗ q.[κ] ={E}=∗
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index 804a287f012764cf3da31b0f5592380d059c12b3..daaeef1baa2125e24d2292cd419bc021b39ee7b0 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -212,10 +212,10 @@ Notation "q .[ κ ]" := (lft_tok q κ)
     (format "q .[ κ ]", at level 0) : uPred_scope.
 Notation "[† κ ]" := (lft_dead κ) (format "[† κ ]"): uPred_scope.
 
-Notation "&{ κ } P" := (bor κ P)
-  (format "&{ κ }  P", at level 20, right associativity) : uPred_scope.
-Notation "&{ κ , i } P" := (idx_bor κ i P)
-  (format "&{ κ , i }  P", at level 20, right associativity) : uPred_scope.
+Notation "&{ κ }" := (bor κ)
+  (format "&{ κ }", at level 20, right associativity) : uPred_scope.
+Notation "&{ κ , i }" := (idx_bor κ i)
+  (format "&{ κ , i }", at level 20, right associativity) : uPred_scope.
 
 Infix "⊑" := lft_incl (at level 70) : uPred_scope.
 
diff --git a/theories/lifetime/model/reborrow.v b/theories/lifetime/model/reborrow.v
index 4706eb2e39c296fdc0ad73f574c03ea50f6343d3..2e7d4d9af3a6f9a6e70a5b304f89c1706070f168 100644
--- a/theories/lifetime/model/reborrow.v
+++ b/theories/lifetime/model/reborrow.v
@@ -160,7 +160,7 @@ Qed.
 
 Lemma idx_bor_unnest E κ κ' i P :
   ↑lftN ⊆ E →
-  lft_ctx -∗ &{κ,i} P -∗ &{κ'} idx_bor_own 1 i ={E}=∗ &{κ ⊓ κ'} P.
+  lft_ctx -∗ &{κ,i} P -∗ &{κ'}(idx_bor_own 1 i) ={E}=∗ &{κ ⊓ κ'} P.
 Proof.
   iIntros (?) "#LFT #HP Hbor".
   rewrite [(&{κ'}_)%I]/bor. iDestruct "Hbor" as (κ'0) "[#Hκ'κ'0 Hbor]".
diff --git a/theories/lifetime/na_borrow.v b/theories/lifetime/na_borrow.v
index 5d17cd6ef7c8f3f689fed1a1322ddd086626bd5b..a43f36fc0f154303f2e4fb1fcae3aedbd9fc5b85 100644
--- a/theories/lifetime/na_borrow.v
+++ b/theories/lifetime/na_borrow.v
@@ -7,8 +7,8 @@ Definition na_bor `{invG Σ, lftG Σ, na_invG Σ}
            (κ : lft) (tid : na_inv_pool_name) (N : namespace) (P : iProp Σ) :=
   (∃ i, &{κ,i}P ∗ na_inv tid N (idx_bor_own 1 i))%I.
 
-Notation "&na{ κ , tid , N } P" := (na_bor κ tid N P)
-  (format "&na{ κ , tid , N }  P", at level 20, right associativity) : uPred_scope.
+Notation "&na{ κ , tid , N }" := (na_bor κ tid N)
+  (format "&na{ κ , tid , N }", at level 20, right associativity) : uPred_scope.
 
 Section na_bor.
   Context `{invG Σ, lftG Σ, na_invG Σ}
diff --git a/theories/typing/lib/cell.v b/theories/typing/lib/cell.v
index 42fb6805fe9ffc69b380bc5142e77b65e69a7038..025d2ef1f61753f39da343304002909783a85454 100644
--- a/theories/typing/lib/cell.v
+++ b/theories/typing/lib/cell.v
@@ -12,7 +12,7 @@ Section cell.
   Program Definition cell (ty : type) :=
     {| ty_size := ty.(ty_size);
        ty_own := ty.(ty_own);
-       ty_shr κ tid l := (&na{κ, tid, shrN.@l}l ↦∗: ty.(ty_own) tid)%I |}.
+       ty_shr κ tid l := (&na{κ, tid, shrN.@l}(l ↦∗: ty.(ty_own) tid))%I |}.
   Next Obligation. apply ty_size_eq. Qed.
   Next Obligation.
     iIntros (ty E κ l tid q ?) "#LFT Hown $". by iApply (bor_na with "Hown").
@@ -146,7 +146,7 @@ Section typing.
       delete [ #1; "c"] ;; delete [ #ty.(ty_size); "x"] ;; return: ["r"].
 
   Lemma cell_replace_type ty `{!TyWf ty} :
-    typed_val (cell_replace ty) (fn(∀ α, ∅; &shr{α} cell ty, ty) → ty).
+    typed_val (cell_replace ty) (fn(∀ α, ∅; &shr{α}(cell ty), ty) → ty).
   Proof.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>c x. simpl_subst.
@@ -178,7 +178,7 @@ Section typing.
     iMod ("Hclose1" with "Htok HL") as "HL".
     (* Now go back to typing level. *)
     iApply (type_type _ _ _
-           [c ◁ box (&shr{α} cell ty); #x ◁ box (uninit ty.(ty_size)); #r ◁ box ty]
+           [c ◁ box (&shr{α}(cell ty)); #x ◁ box (uninit ty.(ty_size)); #r ◁ box ty]
     with "[] LFT HE Htl HL HC"); last first.
     { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
       iFrame "Hc". rewrite !tctx_hasty_val' //. iSplitL "Hx↦ Hx†".
@@ -198,17 +198,17 @@ Section typing.
       delete [ #1; "x"];; return: ["r"].
 
   Lemma fake_shared_cell_type ty `{!TyWf ty} :
-    typed_val fake_shared_cell (fn(∀ α, ∅; &uniq{α} ty) → &shr{α} cell ty).
+    typed_val fake_shared_cell (fn(∀ α, ∅; &uniq{α} ty) → &shr{α}(cell ty)).
   Proof.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iIntros (tid) "#LFT #HE Hna HL Hk HT".
     rewrite tctx_interp_singleton tctx_hasty_val.
-    iApply (type_type _ _ _ [ x ◁ box (&uniq{α}cell ty) ]
+    iApply (type_type _ _ _ [ x ◁ box (&uniq{α}(cell ty)) ]
             with "[] LFT HE Hna HL Hk [HT]"); last first.
     { by rewrite tctx_interp_singleton tctx_hasty_val. }
     iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
-    iApply (type_letalloc_1 (&shr{α}cell ty)); [solve_typing..|]. iIntros (r). simpl_subst.
+    iApply (type_letalloc_1 (&shr{α}(cell ty))); [solve_typing..|]. iIntros (r). simpl_subst.
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
   Qed.
diff --git a/theories/typing/lib/mutex/mutex.v b/theories/typing/lib/mutex/mutex.v
index 18ce32b1a9c3aefffe02180a409c535f5f82a980..58e43755ed86cddb56ed305a54c871d9f9d66149 100644
--- a/theories/typing/lib/mutex/mutex.v
+++ b/theories/typing/lib/mutex/mutex.v
@@ -34,7 +34,7 @@ Section mutex.
            ⌜∃ b, z = Z_of_bool b⌝ ∗ ty.(ty_own) tid vl'
          | _ => False end;
        ty_shr κ tid l := ∃ κ', κ ⊑ κ' ∗
-           &at{κ, mutexN} (lock_proto l (&{κ'} (l +ₗ 1) ↦∗: ty.(ty_own) tid))
+           &at{κ, mutexN} (lock_proto l (&{κ'}((l +ₗ 1) ↦∗: ty.(ty_own) tid)))
     |}%I.
   Next Obligation.
     iIntros (??[|[[]|]]); try iIntros "[]". rewrite ty_size_eq.
@@ -125,7 +125,6 @@ Section mutex.
     iApply heap_mapsto_pred_iff_proper.
     iAlways; iIntros; iSplit; iIntros; by iApply send_change_tid.
   Qed.
-
 End mutex.
 
 Section code.
@@ -217,7 +216,7 @@ Section code.
       return: ["m"].
 
   Lemma mutex_get_mut_type ty `{!TyWf ty} :
-    typed_val mutex_get_mut (fn(∀ α, ∅; &uniq{α} mutex ty) → &uniq{α} ty).
+    typed_val mutex_get_mut (fn(∀ α, ∅; &uniq{α}(mutex ty)) → &uniq{α} ty).
   Proof.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg); inv_vec arg=>m; simpl_subst.
diff --git a/theories/typing/lib/mutex/mutexguard.v b/theories/typing/lib/mutex/mutexguard.v
index e68e4fc3fcef48dd0052ea41f8d98ac50f04fddc..d28626c93aecdd86075a58787c0c2e581616a48d 100644
--- a/theories/typing/lib/mutex/mutexguard.v
+++ b/theories/typing/lib/mutex/mutexguard.v
@@ -35,7 +35,7 @@ Section mguard.
          match vl return _ with
          | [ #(LitLoc l) ] =>
            ∃ β, α ⊑ β ∗
-             &at{α, mutexN} (lock_proto l (&{β} (l +ₗ 1) ↦∗: ty.(ty_own) tid)) ∗
+             &at{α, mutexN} (lock_proto l (&{β} ((l +ₗ 1) ↦∗: ty.(ty_own) tid))) ∗
              &{β} ((l +ₗ 1) ↦∗: ty.(ty_own) tid)
          | _ => False end;
        ty_shr κ tid l :=
@@ -136,8 +136,8 @@ Section code.
 
   Lemma mutex_acc E l ty tid q α κ :
     ↑lftN ⊆ E → ↑mutexN ⊆ E →
-    let R := (&{κ} (l +ₗ 1) ↦∗: ty_own ty tid)%I in
-    lft_ctx -∗ &at{α,mutexN} lock_proto l R -∗ α ⊑ κ -∗
+    let R := (&{κ}((l +ₗ 1) ↦∗: ty_own ty tid))%I in
+    lft_ctx -∗ &at{α,mutexN}(lock_proto l R) -∗ α ⊑ κ -∗
     □ ((q).[α] ={E,∅}=∗ ▷ lock_proto l R ∗ (▷ lock_proto l R ={∅,E}=∗ (q).[α])).
   Proof.
     (* FIXME: This should work: iIntros (?? R). *) intros ?? R.
@@ -157,7 +157,7 @@ Section code.
       delete [ #1; "mutex" ];; return: ["guard"].
 
   Lemma mutex_lock_type ty `{!TyWf ty} :
-    typed_val mutex_lock (fn(∀ α, ∅; &shr{α} mutex ty) → mutexguard α ty).
+    typed_val mutex_lock (fn(∀ α, ∅; &shr{α}(mutex ty)) → mutexguard α ty).
   Proof.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index cb559fbdf1953ec2f1e376ba59c3c5938bce4944..73165f27efc16d321a6a07907a29ea21784b97b2 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -16,7 +16,7 @@ Section ref_functions.
     ∃ (q' : Qp) n, l ↦ #(Zpos n) ∗ ⌜(q ≤ q')%Qc⌝ ∗
             own γ (● Some (to_agree ν, Cinr (q', n)) ⋅ ◯ reading_st q ν) ∗
             ty.(ty_shr) (α ⊓ ν) tid (l +ₗ 1) ∗
-            ((1).[ν] ={↑lftN,∅}▷=∗ &{α} (l +ₗ 1) ↦∗: ty_own ty tid) ∗
+            ((1).[ν] ={↑lftN,∅}▷=∗ &{α}((l +ₗ 1) ↦∗: ty_own ty tid)) ∗
             ∃ q'', ⌜(q' + q'' = 1)%Qp⌝ ∗ q''.[ν].
   Proof.
     iIntros "INV Hâ—¯".
@@ -134,7 +134,7 @@ Section ref_functions.
     iMod ("Hcloseα" with "[$H↦1 $H↦2]") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
     iDestruct (lctx_lft_incl_incl α β with "HL HE") as "#Hαβ"; [solve_typing..|].
     iApply (type_type _ _ _
-        [ x ◁ box (&shr{α} ref β ty); #lv ◁ &shr{α}ty]
+        [ x ◁ box (&shr{α}(ref β ty)); #lv ◁ &shr{α}ty]
         with "[] LFT HE Hna HL Hk"); first last.
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
       iFrame. iApply (ty_shr_mono with "[] Hshr"). by iApply lft_incl_glb. }
diff --git a/theories/typing/lib/refcell/refcell.v b/theories/typing/lib/refcell/refcell.v
index e51da96b50b67f15e9666043ae53e2a2607b0b25..5b7d94c9dc913621f104355ed2e00c22429e901c 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -72,8 +72,8 @@ Section refcell_inv.
     rewrite eqtype_unfold. iIntros (Hty) "HL".
     iDestruct (Hty with "HL") as "#Hty". iIntros "* !# #HE H".
     iDestruct ("Hty" with "HE") as "(% & #Hown & #Hshr)".
-    iAssert (□ (&{α} (l +ₗ 1) ↦∗: ty_own ty1 tid -∗
-                &{α} (l +ₗ 1) ↦∗: ty_own ty2 tid))%I as "#Hb".
+    iAssert (□ (&{α}((l +ₗ 1) ↦∗: ty_own ty1 tid) -∗
+                &{α}((l +ₗ 1) ↦∗: ty_own ty2 tid)))%I as "#Hb".
     { iIntros "!# H". iApply bor_iff; last done.
       iSplit; iIntros "!>!#H"; iDestruct "H" as (vl) "[Hf H]"; iExists vl;
       iFrame; by iApply "Hown". }
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index c372114653cd1a2226065c0abc708940dcdca1fb..acc5cc5b6b0ab94d273889a6b75b1ecccb36c787 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -43,7 +43,7 @@ Section refmut_functions.
     iMod ("Hcloseα1" with "[$H↦1 $H↦2]") as "Hα1".
     iMod ("Hclose''" with "Hβ HL") as "HL". iMod ("Hclose'" with "[$] HL") as "HL".
     iDestruct (lctx_lft_incl_incl α β with "HL HE") as "#Hαβ"; [solve_typing..|].
-    iApply (type_type _ _ _ [ x ◁ box (&shr{α} refmut β ty); #lv ◁ &shr{α}ty]
+    iApply (type_type _ _ _ [ x ◁ box (&shr{α}(refmut β ty)); #lv ◁ &shr{α}ty]
             with "[] LFT HE Hna HL Hk"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
       iFrame. iApply (ty_shr_mono with "[] Hshr'").
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index 5a3ff7ba211ad73c42c7a031123d802c715c2cd8..6b42693d15983748259cfc2ac43edf72cb27233e 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -68,8 +68,8 @@ Section rwlock_inv.
     rewrite eqtype_unfold. iIntros (Hty) "HL".
     iDestruct (Hty with "HL") as "#Hty". iIntros "* !# #HE H".
     iDestruct ("Hty" with "HE") as "(% & #Hown & #Hshr)".
-    iAssert (□ (&{α} (l +ₗ 1) ↦∗: ty_own ty1 tid -∗
-                &{α} (l +ₗ 1) ↦∗: ty_own ty2 tid))%I as "#Hb".
+    iAssert (□ (&{α}((l +ₗ 1) ↦∗: ty_own ty1 tid) -∗
+                &{α}((l +ₗ 1) ↦∗: ty_own ty2 tid)))%I as "#Hb".
     { iIntros "!# H". iApply bor_iff; last done.
       iSplit; iIntros "!>!#H"; iDestruct "H" as (vl) "[Hf H]"; iExists vl;
       iFrame; by iApply "Hown". }
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index 3a345f9697a09bfad1ab1989798cc1cec169ce03..6ad1ecb4c9aeb13f5213f47413d3414a6a30abe3 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -60,8 +60,8 @@ Section sum.
                                 (nth i tyl emp0).(ty_own) tid vl')%I;
        ty_shr κ tid l :=
          (∃ (i : nat),
-             (&frac{κ} λ q, l ↦{q} #i ∗
-                       (l +ₗ (S $ (nth i tyl emp0).(ty_size))) ↦∗{q}: is_pad i tyl) ∗
+           &frac{κ} (λ q, l ↦{q} #i ∗
+                     (l +ₗ (S $ (nth i tyl emp0).(ty_size))) ↦∗{q}: is_pad i tyl) ∗
                (nth i tyl emp0).(ty_shr) κ tid (l +ₗ 1))%I
     |}.
   Next Obligation.
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 9bcb847f67c12eb2bd80ccd2c3e3fff26c9ba45f..2fb6b46e53dc604c5236035f908c747f064c6c4b 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -126,8 +126,7 @@ Program Definition ty_of_st `{typeG Σ} (st : simple_type) : type :=
          borrow, otherwise I do not know how to prove the shr part of
          [subtype_shr_mono]. *)
      ty_shr := λ κ tid l,
-               (∃ vl, (&frac{κ} λ q, l ↦∗{q} vl) ∗
-                                                 â–· st.(st_own) tid vl)%I
+               (∃ vl, &frac{κ} (λ q, l ↦∗{q} vl) ∗ ▷ st.(st_own) tid vl)%I
   |}.
 Next Obligation. intros. apply st_size_eq. Qed.
 Next Obligation.
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index 5a3a55433fa462651d1216023c52d1f8482f793a..c0fca1b285ccd6b08ffd823e8974830c77b1f773 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -12,7 +12,7 @@ Section uniq_bor.
     {| ty_size := 1;
        ty_own tid vl :=
          match vl return _ with
-         | [ #(LitLoc l) ] => &{κ} l ↦∗: ty.(ty_own) tid
+         | [ #(LitLoc l) ] => &{κ} (l ↦∗: ty.(ty_own) tid)
          | _ => False
          end;
        ty_shr κ' tid l :=
diff --git a/theories/typing/util.v b/theories/typing/util.v
index fec9517556eb9deb80d3bf19fc0573801bd822f8..1b907a641b09243d71b38c29790f423482ca339f 100644
--- a/theories/typing/util.v
+++ b/theories/typing/util.v
@@ -27,7 +27,7 @@ Section util.
 
   Lemma delay_sharing_later N κ l ty tid :
     lftE ⊆ N →
-    lft_ctx -∗ &{κ} ▷ l ↦∗: ty_own ty tid ={N}=∗
+    lft_ctx -∗ &{κ}(▷ l ↦∗: ty_own ty tid) ={N}=∗
        □ ∀ (F : coPset) (q : Qp),
        ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ (q).[κ] ={F,F ∖ ↑shrN}▷=∗ ty.(ty_shr) κ tid l ∗ (q).[κ].
   Proof.
@@ -49,7 +49,7 @@ Section util.
 
   Lemma delay_sharing_nested N κ κ' κ'' l ty tid :
     lftE ⊆ N →
-    lft_ctx -∗ ▷ (κ'' ⊑ κ ⊓ κ') -∗ &{κ'} &{κ} l ↦∗: ty_own ty tid ={N}=∗
+    lft_ctx -∗ ▷ (κ'' ⊑ κ ⊓ κ') -∗ &{κ'}(&{κ}(l ↦∗: ty_own ty tid)) ={N}=∗
        □ ∀ (F : coPset) (q : Qp),
        ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ (q).[κ''] ={F,F ∖ ↑shrN}▷=∗ ty.(ty_shr) κ'' tid l ∗ (q).[κ''].
   Proof.