diff --git a/theories/lifetime/at_borrow.v b/theories/lifetime/at_borrow.v
index 3ce37b766398dbf5a2e57ebdd4cbd0d52df5d908..4148b93e8c6817f8e368232fc1ad9cc64d80877f 100644
--- a/theories/lifetime/at_borrow.v
+++ b/theories/lifetime/at_borrow.v
@@ -9,8 +9,7 @@ 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 }" := (at_bor κ N)
-  (format "&at{ κ , N }", at level 20, right associativity) : uPred_scope.
+Notation "&at{ κ , N }" := (at_bor κ N) (format "&at{ κ , N }") : uPred_scope.
 
 Section atomic_bors.
   Context `{invG Σ, lftG Σ} (P : iProp Σ) (N : namespace).
diff --git a/theories/lifetime/frac_borrow.v b/theories/lifetime/frac_borrow.v
index eb8513025e581cc45efd8ad4392c54cef5afe17f..d700003cc32b5fe38a0d9873350941e2e06db6c8 100644
--- a/theories/lifetime/frac_borrow.v
+++ b/theories/lifetime/frac_borrow.v
@@ -10,8 +10,7 @@ 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{ κ }" := (frac_bor κ)
-  (format "&frac{ κ }", at level 20, right associativity) : uPred_scope.
+Notation "&frac{ κ }" := (frac_bor κ) (format "&frac{ κ }") : uPred_scope.
 
 Section frac_bor.
   Context `{invG Σ, lftG Σ, frac_borG Σ} (φ : Qp → iProp Σ).
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index e370a2b7d9e263d299fa318cf4a02e3dcc7453d6..af69eaed4e0503b63a0d2553d041b8b8602979e3 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -39,10 +39,8 @@ Module Type lifetime_sig.
       (format "q .[ κ ]", at level 0) : uPred_scope.
   Notation "[† κ ]" := (lft_dead κ) (format "[† κ ]"): 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.
+  Notation "&{ κ }" := (bor κ) (format "&{ κ }") : uPred_scope.
+  Notation "&{ κ , i }" := (idx_bor κ i) (format "&{ κ , i }") : uPred_scope.
 
   Infix "⊑" := lft_incl (at level 70) : uPred_scope.
   Infix "⊓" := lft_intersect (at level 40) : C_scope.
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index daaeef1baa2125e24d2292cd419bc021b39ee7b0..41545ef98b54bc8f0c1e275d85cc79005c57b4a1 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -212,10 +212,8 @@ Notation "q .[ κ ]" := (lft_tok q κ)
     (format "q .[ κ ]", at level 0) : uPred_scope.
 Notation "[† κ ]" := (lft_dead κ) (format "[† κ ]"): 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.
+Notation "&{ κ }" := (bor κ) (format "&{ κ }") : uPred_scope.
+Notation "&{ κ , i }" := (idx_bor κ i) (format "&{ κ , i }") : uPred_scope.
 
 Infix "⊑" := lft_incl (at level 70) : uPred_scope.
 
diff --git a/theories/lifetime/na_borrow.v b/theories/lifetime/na_borrow.v
index a43f36fc0f154303f2e4fb1fcae3aedbd9fc5b85..64adfc2cfaae777f01219abe30ef10a7951fe46d 100644
--- a/theories/lifetime/na_borrow.v
+++ b/theories/lifetime/na_borrow.v
@@ -8,7 +8,7 @@ Definition na_bor `{invG Σ, lftG Σ, na_invG Σ}
   (∃ i, &{κ,i}P ∗ na_inv tid N (idx_bor_own 1 i))%I.
 
 Notation "&na{ κ , tid , N }" := (na_bor κ tid N)
-  (format "&na{ κ , tid , N }", at level 20, right associativity) : uPred_scope.
+    (format "&na{ κ , tid , N }") : uPred_scope.
 
 Section na_bor.
   Context `{invG Σ, lftG Σ, na_invG Σ}
diff --git a/theories/typing/borrow.v b/theories/typing/borrow.v
index 5f13cdd3a842578530eacbdc12369bbee9a57c1b..1fe107e0e624d58166b6a108ab445f429569b2a0 100644
--- a/theories/typing/borrow.v
+++ b/theories/typing/borrow.v
@@ -44,7 +44,7 @@ Section borrow.
 
   Lemma type_deref_uniq_own_instr {E L} κ p n ty :
     lctx_lft_alive E L κ →
-    typed_instruction_ty E L [p ◁ &uniq{κ} own_ptr n ty] (!p) (&uniq{κ} ty).
+    typed_instruction_ty E L [p ◁ &uniq{κ}(own_ptr n ty)] (!p) (&uniq{κ} ty).
   Proof.
     iIntros (Hκ tid) "#LFT HE $ HL Hp".
     rewrite tctx_interp_singleton.
@@ -66,15 +66,15 @@ Section borrow.
 
   Lemma type_deref_uniq_own {E L} κ x p e n ty C T T' :
     Closed (x :b: []) e →
-    tctx_extract_hasty E L p (&uniq{κ} own_ptr n ty) T T' →
+    tctx_extract_hasty E L p (&uniq{κ}(own_ptr n ty)) T T' →
     lctx_lft_alive E L κ →
-    (∀ (v:val), typed_body E L C ((v ◁ &uniq{κ} ty) :: T') (subst' x v e)) -∗
+    (∀ (v:val), typed_body E L C ((v ◁ &uniq{κ}ty) :: T') (subst' x v e)) -∗
     typed_body E L C T (let: x := !p in e).
   Proof. iIntros. iApply type_let; [by apply type_deref_uniq_own_instr|solve_typing|done]. Qed.
 
   Lemma type_deref_shr_own_instr {E L} κ p n ty :
     lctx_lft_alive E L κ →
-    typed_instruction_ty E L [p ◁ &shr{κ} own_ptr n ty] (!p) (&shr{κ} ty).
+    typed_instruction_ty E L [p ◁ &shr{κ}(own_ptr n ty)] (!p) (&shr{κ} ty).
   Proof.
     iIntros (Hκ tid) "#LFT HE $ HL Hp".
     rewrite tctx_interp_singleton.
@@ -92,7 +92,7 @@ Section borrow.
 
   Lemma type_deref_shr_own {E L} κ x p e n ty C T T' :
     Closed (x :b: []) e →
-    tctx_extract_hasty E L p (&shr{κ} own_ptr n ty) T T' →
+    tctx_extract_hasty E L p (&shr{κ}(own_ptr n ty)) T T' →
     lctx_lft_alive E L κ →
     (∀ (v:val), typed_body E L C ((v ◁ &shr{κ} ty) :: T') (subst' x v e)) -∗
     typed_body E L C T (let: x := !p in e).
@@ -100,7 +100,7 @@ Section borrow.
 
   Lemma type_deref_uniq_uniq_instr {E L} κ κ' p ty :
     lctx_lft_alive E L κ → lctx_lft_incl E L κ κ' →
-    typed_instruction_ty E L [p ◁ &uniq{κ} &uniq{κ'} ty] (!p) (&uniq{κ} ty).
+    typed_instruction_ty E L [p ◁ &uniq{κ}(&uniq{κ'}ty)] (!p) (&uniq{κ} ty).
   Proof.
     iIntros (Hκ Hincl tid) "#LFT #HE $ HL Hp".
     rewrite tctx_interp_singleton.
@@ -124,15 +124,15 @@ Section borrow.
 
   Lemma type_deref_uniq_uniq {E L} κ κ' x p e ty C T T' :
     Closed (x :b: []) e →
-    tctx_extract_hasty E L p (&uniq{κ} &uniq{κ'} ty) T T' →
+    tctx_extract_hasty E L p (&uniq{κ}(&uniq{κ'}ty))%T T T' →
     lctx_lft_alive E L κ → lctx_lft_incl E L κ κ' →
-    (∀ (v:val), typed_body E L C ((v ◁ &uniq{κ} ty) :: T') (subst' x v e)) -∗
+    (∀ (v:val), typed_body E L C ((v ◁ &uniq{κ}ty) :: T') (subst' x v e)) -∗
     typed_body E L C T (let: x := !p in e).
   Proof. iIntros. iApply type_let; [by apply type_deref_uniq_uniq_instr|solve_typing|done]. Qed.
 
   Lemma type_deref_shr_uniq_instr {E L} κ κ' p ty :
     lctx_lft_alive E L κ → lctx_lft_incl E L κ κ' →
-    typed_instruction_ty E L [p ◁ &shr{κ} &uniq{κ'} ty] (!p) (&shr{κ} ty).
+    typed_instruction_ty E L [p ◁ &shr{κ}(&uniq{κ'}ty)] (!p) (&shr{κ}ty).
   Proof.
     iIntros (Hκ Hincl tid) "#LFT HE $ HL Hp". rewrite tctx_interp_singleton.
     iDestruct (Hincl with "HL HE") as "#Hincl".
@@ -155,9 +155,9 @@ Section borrow.
 
   Lemma type_deref_shr_uniq {E L} κ κ' x p e ty C T T' :
     Closed (x :b: []) e →
-    tctx_extract_hasty E L p (&shr{κ} &uniq{κ'} ty) T T' →
+    tctx_extract_hasty E L p (&shr{κ}(&uniq{κ'}ty))%T T T' →
     lctx_lft_alive E L κ → lctx_lft_incl E L κ κ' →
-    (∀ (v:val), typed_body E L C ((v ◁ &shr{κ} ty) :: T') (subst' x v e)) -∗
+    (∀ (v:val), typed_body E L C ((v ◁ &shr{κ}ty) :: T') (subst' x v e)) -∗
     typed_body E L C T (let: x := !p in e).
   Proof. iIntros. iApply type_let; [by apply type_deref_shr_uniq_instr|solve_typing|done]. Qed.
 End borrow.
diff --git a/theories/typing/examples/get_x.v b/theories/typing/examples/get_x.v
index 66fef27d074343423ea84d867079909a2a7fabdd..3052ba5a7a8f0be9d049654bb3f02baa2939c751 100644
--- a/theories/typing/examples/get_x.v
+++ b/theories/typing/examples/get_x.v
@@ -12,7 +12,7 @@ Section get_x.
        delete [ #1; "p"] ;; return: ["r"].
 
   Lemma get_x_type :
-    typed_val get_x (fn(∀ α, ∅; &uniq{α} Π[int; int]) → &shr{α} int).
+    typed_val get_x (fn(∀ α, ∅; &uniq{α}(Π[int; int])) → &shr{α}int).
   Proof.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ϝ ret p).
     inv_vec p=>p. simpl_subst.
diff --git a/theories/typing/examples/rebor.v b/theories/typing/examples/rebor.v
index 4efa575329c5b7342a9457c0d3636ba428bd9d5b..c8b0b12783079550d086e9b1006c0f88b73314bc 100644
--- a/theories/typing/examples/rebor.v
+++ b/theories/typing/examples/rebor.v
@@ -22,10 +22,10 @@ Section rebor.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([] ϝ ret p). inv_vec p=>t1 t2. simpl_subst.
     iApply (type_newlft []). iIntros (α).
-    iApply (type_letalloc_1 (&uniq{α}Π[int; int])); [solve_typing..|]. iIntros (x). simpl_subst.
+    iApply (type_letalloc_1 (&uniq{α}(Π[int; int]))); [solve_typing..|]. iIntros (x). simpl_subst.
     iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
     iApply (type_letpath (&uniq{α}int)); [solve_typing|]. iIntros (y). simpl_subst.
-    iApply (type_assign _ (&uniq{α}Π [int; int])); [solve_typing..|].
+    iApply (type_assign _ (&uniq{α}(Π[int; int]))); [solve_typing..|].
     iApply type_deref; [solve_typing..|]. iIntros (y'). simpl_subst.
     iApply type_letalloc_1; [solve_typing..|]. iIntros (r). simpl_subst.
     iApply type_endlft.
diff --git a/theories/typing/examples/unbox.v b/theories/typing/examples/unbox.v
index 7b19d4be356eed375d7f2c8cade36aa1ed4f5092..cb63526d34ebc2b63732a86702ea240a95562378 100644
--- a/theories/typing/examples/unbox.v
+++ b/theories/typing/examples/unbox.v
@@ -12,7 +12,7 @@ Section unbox.
        delete [ #1; "b"] ;; return: ["r"].
 
   Lemma ubox_type :
-    typed_val unbox (fn(∀ α, ∅; &uniq{α}box (Π[int; int])) → &uniq{α} int).
+    typed_val unbox (fn(∀ α, ∅; &uniq{α}(box(Π[int; int]))) → &uniq{α}int).
   Proof.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret b). inv_vec b=>b. simpl_subst.
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index 249e6cc772b0be46d8b51f924966f7cf1fce3671..290ec5e953a234e1356afc6acc63e36cd1ceaf81 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -418,7 +418,7 @@ Section arc.
       delete [ #1; "arc" ];; return: ["x"].
 
   Lemma arc_deref_type ty `{!TyWf ty} :
-    typed_val arc_deref (fn(∀ α, ∅; &shr{α} arc ty) → &shr{α} ty).
+    typed_val arc_deref (fn(∀ α, ∅; &shr{α}(arc ty)) → &shr{α}ty).
   Proof.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>rcx. simpl_subst.
@@ -443,7 +443,7 @@ Section arc.
       iDestruct (lft_tok_dead with "Hα1 Hα†") as "[]". }
     wp_op. wp_write. iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
     (* Finish up the proof. *)
-    iApply (type_type _ _ _ [ rcx ◁ box (&shr{α} arc ty); #lrc2 ◁ box (&shr{α} ty)]
+    iApply (type_type _ _ _ [ rcx ◁ box (&shr{α}(arc ty)); #lrc2 ◁ box (&shr{α}ty)]
         with "[] LFT HE Hna HL Hk [-]"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val tctx_hasty_val' //.
       unlock. iFrame "Hrcx". iFrame "Hx†". iExists [_]. rewrite heap_mapsto_vec_singleton.
@@ -462,7 +462,7 @@ Section arc.
       delete [ #1; "arc" ];; return: ["r"].
 
   Lemma arc_strong_count_type ty `{!TyWf ty} :
-    typed_val arc_strong_count (fn(∀ α, ∅; &shr{α} arc ty) → int).
+    typed_val arc_strong_count (fn(∀ α, ∅; &shr{α}(arc ty)) → int).
   Proof.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
@@ -487,7 +487,7 @@ Section arc.
       iIntros "Htok". iMod "Hclose2" as "_". by iApply "Hclose1". }
     iIntros (c) "[Hα _]". iMod ("Hclose1" with "Hα HL") as "HL".
     (* Finish up the proof. *)
-    iApply (type_type _ _ _ [ x ◁ box (&shr{α} arc ty); #c ◁ int; r ◁ box (uninit 1)]
+    iApply (type_type _ _ _ [ x ◁ box (&shr{α}(arc ty)); #c ◁ int; r ◁ box (uninit 1)]
         with "[] LFT HE Hna HL Hk [-]"); last first.
     { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val tctx_hasty_val' //.
       unlock. iFrame. }
@@ -505,7 +505,7 @@ Section arc.
       delete [ #1; "arc" ];; return: ["r"].
 
   Lemma arc_weak_count_type ty `{!TyWf ty} :
-    typed_val arc_weak_count (fn(∀ α, ∅; &shr{α} arc ty) → int).
+    typed_val arc_weak_count (fn(∀ α, ∅; &shr{α}(arc ty)) → int).
   Proof.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
@@ -530,7 +530,7 @@ Section arc.
       iIntros "Htok". iMod "Hclose2" as "_". by iApply "Hclose1". }
     iIntros (c) "[Hα _]". iMod ("Hclose1" with "Hα HL") as "HL".
     (* Finish up the proof. *)
-    iApply (type_type _ _ _ [ x ◁ box (&shr{α} arc ty); #c ◁ int; r ◁ box (uninit 1)]
+    iApply (type_type _ _ _ [ x ◁ box (&shr{α}(arc ty)); #c ◁ int; r ◁ box (uninit 1)]
         with "[] LFT HE Hna HL Hk [-]"); last first.
     { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val tctx_hasty_val' //.
       unlock. iFrame. }
@@ -550,7 +550,7 @@ Section arc.
       delete [ #1; "arc" ];; return: ["r"].
 
   Lemma arc_clone_type ty `{!TyWf ty} :
-    typed_val arc_clone (fn(∀ α, ∅; &shr{α} arc ty) → arc ty).
+    typed_val arc_clone (fn(∀ α, ∅; &shr{α}(arc ty)) → arc ty).
   Proof.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
@@ -575,7 +575,7 @@ Section arc.
       iIntros "Htok". iMod "Hclose2" as "_". by iApply "Hclose1". }
     iIntros (q'') "[Hα Hown]". wp_seq. iMod ("Hclose1" with "Hα HL") as "HL".
     (* Finish up the proof. *)
-    iApply (type_type _ _ _ [ x ◁ box (&shr{α} arc ty); #l' ◁ arc ty; r ◁ box (uninit 1)]
+    iApply (type_type _ _ _ [ x ◁ box (&shr{α}(arc ty)); #l' ◁ arc ty; r ◁ box (uninit 1)]
         with "[] LFT HE Hna HL Hk [-]"); last first.
     { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val tctx_hasty_val' //.
       unlock. iFrame. simpl. unfold shared_arc_own. auto 10 with iFrame. }
@@ -594,7 +594,7 @@ Section arc.
       delete [ #1; "w" ];; return: ["r"].
 
   Lemma weak_clone_type ty `{!TyWf ty} :
-    typed_val weak_clone (fn(∀ α, ∅; &shr{α} weak ty) → weak ty).
+    typed_val weak_clone (fn(∀ α, ∅; &shr{α}(weak ty)) → weak ty).
   Proof.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
@@ -619,7 +619,7 @@ Section arc.
       iIntros "Htok". iMod "Hclose2" as "_". by iApply "Hclose1". }
     iIntros "[Hα Hown]". wp_seq. iMod ("Hclose1" with "Hα HL") as "HL".
     (* Finish up the proof. *)
-    iApply (type_type _ _ _ [ x ◁ box (&shr{α} weak ty); #l' ◁ weak ty; r ◁ box (uninit 1) ]
+    iApply (type_type _ _ _ [ x ◁ box (&shr{α}(weak ty)); #l' ◁ weak ty; r ◁ box (uninit 1) ]
         with "[] LFT HE Hna HL Hk [-]"); last first.
     { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val tctx_hasty_val' //.
       unlock. iFrame. simpl. eauto 10 with iFrame. }
@@ -638,7 +638,7 @@ Section arc.
       delete [ #1; "arc" ];; return: ["r"].
 
   Lemma downgrade_type ty `{!TyWf ty} :
-    typed_val downgrade (fn(∀ α, ∅; &shr{α} arc ty) → weak ty).
+    typed_val downgrade (fn(∀ α, ∅; &shr{α}(arc ty)) → weak ty).
   Proof.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
@@ -663,7 +663,7 @@ Section arc.
       iIntros "Htok". iMod "Hclose2" as "_". by iApply "Hclose1". }
     iIntros "[Hα Hown]". wp_seq. iMod ("Hclose1" with "Hα HL") as "HL".
     (* Finish up the proof. *)
-    iApply (type_type _ _ _ [ x ◁ box (&shr{α} arc ty); #l' ◁ weak ty; r ◁ box (uninit 1) ]
+    iApply (type_type _ _ _ [ x ◁ box (&shr{α}(arc ty)); #l' ◁ weak ty; r ◁ box (uninit 1) ]
         with "[] LFT HE Hna HL Hk [-]"); last first.
     { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val tctx_hasty_val' //.
       unlock. iFrame. simpl. eauto 10 with iFrame. }
@@ -685,7 +685,7 @@ Section arc.
         delete [ #1; "w" ];; return: ["r"].
 
   Lemma upgrade_type ty `{!TyWf ty} :
-    typed_val upgrade (fn(∀ α, ∅; &shr{α} weak ty) → option (arc ty)).
+    typed_val upgrade (fn(∀ α, ∅; &shr{α}(weak ty)) → option (arc ty)).
   Proof.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
@@ -710,7 +710,7 @@ Section arc.
       iIntros "Htok". iMod "Hclose2" as "_". by iApply "Hclose1". }
     iIntros ([] q') "[Hα Hown]"; wp_if; iMod ("Hclose1" with "Hα HL") as "HL".
     - (* Finish up the proof (sucess). *)
-      iApply (type_type _ _ _ [ x ◁ box (&shr{α} weak ty); #l' ◁ arc ty;
+      iApply (type_type _ _ _ [ x ◁ box (&shr{α}(weak ty)); #l' ◁ arc ty;
                                 r ◁ box (uninit 2) ]
               with "[] LFT HE Hna HL Hk [-]"); last first.
       { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val tctx_hasty_val' //.
@@ -719,7 +719,7 @@ Section arc.
       iApply type_delete; [solve_typing..|].
       iApply type_jump; solve_typing.
     - (* Finish up the proof (fail). *)
-      iApply (type_type _ _ _ [ x ◁ box (&shr{α} weak ty); r ◁ box (uninit 2) ]
+      iApply (type_type _ _ _ [ x ◁ box (&shr{α}(weak ty)); r ◁ box (uninit 2) ]
               with "[] LFT HE Hna HL Hk [-]"); last first.
       { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
         unlock. iFrame. }
@@ -920,7 +920,7 @@ Section arc.
         delete [ #1; "arc"];; return: ["r"].
 
   Lemma arc_get_mut_type ty `{!TyWf ty} :
-    typed_val arc_get_mut (fn(∀ α, ∅; &uniq{α} arc ty) → option (&uniq{α}ty)).
+    typed_val arc_get_mut (fn(∀ α, ∅; &uniq{α}(arc ty)) → option (&uniq{α}ty)).
   Proof.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
     iIntros (α ϝ ret arg). inv_vec arg=>rcx. simpl_subst.
@@ -1006,8 +1006,8 @@ Section arc.
        ]).
 
   Lemma arc_make_mut_type ty `{!TyWf ty} clone :
-    typed_val clone (fn(∀ α, ∅; &shr{α} ty) → ty) →
-    typed_val (arc_make_mut ty clone) (fn(∀ α, ∅; &uniq{α} arc ty) → &uniq{α} ty).
+    typed_val clone (fn(∀ α, ∅; &shr{α}ty) → ty) →
+    typed_val (arc_make_mut ty clone) (fn(∀ α, ∅; &uniq{α}(arc ty)) → &uniq{α} ty).
   Proof.
     intros Hclone E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
     iIntros (α ϝ ret arg). inv_vec arg=>rcx. simpl_subst.
diff --git a/theories/typing/lib/fake_shared_box.v b/theories/typing/lib/fake_shared_box.v
index 768aabdd2a1787edb6c50fa44ea71bb0e2118474..99530965643368fbd0a1ebbd5abfcbaf346ec303 100644
--- a/theories/typing/lib/fake_shared_box.v
+++ b/theories/typing/lib/fake_shared_box.v
@@ -11,14 +11,14 @@ Section fake_shared_box.
 
   Lemma fake_shared_box_type ty `{!TyWf ty} :
     typed_val fake_shared_box
-      (fn(∀ '(α, β), ∅; &shr{α} &shr{β} ty) → &shr{α} box ty).
+      (fn(∀ '(α, β), ∅; &shr{α}(&shr{β} ty)) → &shr{α}(box 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.
     iDestruct (lctx_lft_incl_incl α β with "HL HE") as "#Hαβ"; [solve_typing..|].
-    iAssert (▷ ty_own (own_ptr 1 (&shr{α} box ty)) tid [x])%I with "[HT]" as "HT".
+    iAssert (▷ ty_own (own_ptr 1 (&shr{α}(box ty))) tid [x])%I with "[HT]" as "HT".
     { destruct x as [[|l|]|]=>//=. iDestruct "HT" as "[H $]".
       iNext. iDestruct "H" as ([|[[]|][]]) "[H↦ H]"; try done.
       iExists _. iFrame. iDestruct "H" as (vl) "[#Hf H]".
@@ -28,7 +28,7 @@ Section fake_shared_box.
       iDestruct "H" as "#H". iIntros "!# * % $". iApply step_fupd_intro. set_solver.
       by iApply ty_shr_mono. }
     wp_seq.
-    iApply (type_type [] _ _ [ x ◁ box (&shr{α}box ty) ]
+    iApply (type_type [] _ _ [ x ◁ box (&shr{α}(box ty)) ]
             with "[] LFT [] Hna HL Hk [HT]"); last first.
     { by rewrite tctx_interp_singleton tctx_hasty_val. }
     { by rewrite /elctx_interp. }
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index 4254db321470fa35ee0d226f506264c88317bb02..123029972f8c15f41b31ecf44f6ad81cf3400138 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -379,7 +379,7 @@ Section code.
       delete [ #1; "rc" ];; return: ["r"].
 
   Lemma rc_strong_count_type ty `{!TyWf ty} :
-    typed_val rc_strong_count (fn(∀ α, ∅; &shr{α} rc ty) → int).
+    typed_val rc_strong_count (fn(∀ α, ∅; &shr{α}(rc ty)) → int).
   Proof.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
@@ -415,7 +415,7 @@ Section code.
     { iExists _. iFrame "Hrc●". iExists _. auto with iFrame. }
     iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
     (* Finish up the proof. *)
-    iApply (type_type _ _ _ [ x ◁ box (&shr{α} rc ty); r ◁ box (uninit 1);
+    iApply (type_type _ _ _ [ x ◁ box (&shr{α}(rc ty)); r ◁ box (uninit 1);
                               #(Z.pos s0) ◁ int ]
         with "[] LFT HE Hna HL Hk [-]"); last first.
     { unlock.
@@ -438,7 +438,7 @@ Section code.
       delete [ #1; "rc" ];; return: ["r"].
 
   Lemma rc_weak_count_type ty `{!TyWf ty} :
-    typed_val rc_weak_count (fn(∀ α, ∅; &shr{α} rc ty) → int).
+    typed_val rc_weak_count (fn(∀ α, ∅; &shr{α}(rc ty)) → int).
   Proof.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
@@ -474,7 +474,7 @@ Section code.
     { iExists _. iFrame "Hrc●". iExists _. auto with iFrame. }
     iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
     (* Finish up the proof. *)
-    iApply (type_type _ _ _ [ x ◁ box (&shr{α} rc ty); r ◁ box (uninit 1);
+    iApply (type_type _ _ _ [ x ◁ box (&shr{α}(rc ty)); r ◁ box (uninit 1);
                               #(S weak) ◁ int ]
         with "[] LFT HE Hna HL Hk [-]"); last first.
     { unlock.
@@ -541,7 +541,7 @@ Section code.
       delete [ #1; "rc" ];; return: ["r"].
 
   Lemma rc_clone_type ty `{!TyWf ty} :
-    typed_val rc_clone (fn(∀ α, ∅; &shr{α} rc ty) → rc ty).
+    typed_val rc_clone (fn(∀ α, ∅; &shr{α}(rc ty)) → rc ty).
   Proof.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
@@ -587,7 +587,7 @@ Section code.
       rewrite [_ â‹… _]comm frac_op' -[(_ + _)%Qp]assoc Qp_div_2. auto. }
     iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
     (* Finish up the proof. *)
-    iApply (type_type _ _ _ [ x ◁ box (&shr{α} rc ty); #lr ◁ box (rc ty)]
+    iApply (type_type _ _ _ [ x ◁ box (&shr{α}(rc ty)); #lr ◁ box (rc ty)]
         with "[] LFT HE Hna HL Hk [-]"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
       unlock. iFrame "Hx". iFrame "Hr†". iExists [# #l'].
@@ -604,7 +604,7 @@ Section code.
       delete [ #1; "rc" ];; return: ["x"].
 
   Lemma rc_deref_type ty `{!TyWf ty} :
-    typed_val rc_deref (fn(∀ α, ∅; &shr{α} rc ty) → &shr{α} ty).
+    typed_val rc_deref (fn(∀ α, ∅; &shr{α}(rc ty)) → &shr{α}ty).
   Proof.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>rcx. simpl_subst.
@@ -629,7 +629,7 @@ Section code.
       iDestruct (lft_tok_dead with "Hα1 Hα†") as "[]". }
     wp_op. wp_write. iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
     (* Finish up the proof. *)
-    iApply (type_type _ _ _ [ rcx ◁ box (&shr{α} rc ty); #lrc2 ◁ box (&shr{α} ty)]
+    iApply (type_type _ _ _ [ rcx ◁ box (&shr{α}(rc ty)); #lrc2 ◁ box (&shr{α}ty)]
         with "[] LFT HE Hna HL Hk [-]"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val tctx_hasty_val' //.
       unlock. iFrame "Hrcx". iFrame "Hx†". iExists [_]. rewrite heap_mapsto_vec_singleton.
@@ -852,13 +852,13 @@ Section code.
       delete [ #1; "rc"];; return: ["r"].
 
   Lemma rc_get_mut_type ty `{!TyWf ty} :
-    typed_val rc_get_mut (fn(∀ α, ∅; &uniq{α} rc ty) → option (&uniq{α} ty)).
+    typed_val rc_get_mut (fn(∀ α, ∅; &uniq{α}(rc ty)) → option (&uniq{α}ty)).
   Proof.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>rcx. simpl_subst.
     iApply (type_new 2); [solve_typing..|]; iIntros (r); simpl_subst.
     iApply (type_cont [] [ϝ ⊑ₗ []]
-                      (λ _, [rcx ◁ box (uninit 1); r ◁ box (option $ &uniq{α} ty)]));
+                      (λ _, [rcx ◁ box (uninit 1); r ◁ box (option $ &uniq{α}ty)]));
       [solve_typing..| |]; last first.
     { simpl. iAlways. iIntros (k arg). inv_vec arg. simpl_subst.
       iApply type_delete; [solve_typing..|].
@@ -887,12 +887,12 @@ Section code.
         { iIntros "!> Hty". iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame "Hrc'".
           iLeft. by iFrame. }
         iMod ("Hclose1" with "Hα HL") as "HL".
-        iApply (type_type _ _ _ [ r ◁ box (uninit 2); #l +ₗ #2 ◁ &uniq{α} ty;
+        iApply (type_type _ _ _ [ r ◁ box (uninit 2); #l +ₗ #2 ◁ &uniq{α}ty;
                                   rcx ◁ box (uninit 1)]
                 with "[] LFT HE Hna HL Hk [-]"); last first.
         { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val tctx_hasty_val' //.
           unlock. iFrame. }
-        iApply (type_sum_assign (option (&uniq{_} _))); [solve_typing..|].
+        iApply (type_sum_assign (option (&uniq{_}_))); [solve_typing..|].
         iApply type_jump; solve_typing.
       + wp_op=>[?|_]; first lia. wp_if. iMod ("Hrc" with "Hl1 Hl2") as "[Hna Hrc]".
         iMod ("Hclose2" with "[] [Hrc' Hrc]") as "[Hrc' Hα]".
@@ -903,7 +903,7 @@ Section code.
                 with "[] LFT HE Hna HL Hk [-]"); last first.
         { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
           unlock. iFrame. }
-        iApply (type_sum_unit (option (&uniq{_} _))); [solve_typing..|].
+        iApply (type_sum_unit (option (&uniq{_}_))); [solve_typing..|].
         iApply type_jump; solve_typing.
     - wp_if. iDestruct "Hc" as "[[% _]|[% [Hproto _]]]"; first lia.
       iMod ("Hproto" with "Hl1") as "[Hna Hrc]".
@@ -915,7 +915,7 @@ Section code.
               with "[] LFT HE Hna HL Hk [-]"); last first.
       { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
         unlock. iFrame. }
-      iApply (type_sum_unit (option (&uniq{_} _))); [solve_typing..|].
+      iApply (type_sum_unit (option (&uniq{_}_))); [solve_typing..|].
       iApply type_jump; solve_typing.
   Qed.
 
@@ -982,14 +982,14 @@ Section code.
 
   Lemma rc_make_mut_type ty `{!TyWf ty} clone :
     (* ty : Clone, as witnessed by the impl clone *)
-    typed_val clone (fn(∀ α, ∅; &shr{α} ty) → ty) →
-    typed_val (rc_make_mut ty clone) (fn(∀ α, ∅; &uniq{α} rc ty) → &uniq{α} ty).
+    typed_val clone (fn(∀ α, ∅; &shr{α}ty) → ty) →
+    typed_val (rc_make_mut ty clone) (fn(∀ α, ∅; &uniq{α}(rc ty)) → &uniq{α}ty).
   Proof.
     intros Hclone E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>rcx. simpl_subst.
     iApply (type_new 1); [solve_typing..|]; iIntros (r); simpl_subst.
     iApply (type_cont [] [ϝ ⊑ₗ []]
-                      (λ _, [rcx ◁ box (uninit 1); r ◁ box (&uniq{α} ty)]));
+                      (λ _, [rcx ◁ box (uninit 1); r ◁ box (&uniq{α}ty)]));
       [solve_typing..| |]; last first.
     { simpl. iAlways. iIntros (k arg). inv_vec arg. simpl_subst.
       iApply type_delete; [solve_typing..|].
@@ -1018,7 +1018,7 @@ Section code.
         { iIntros "!> Hty". iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame "Hrc'".
           iLeft. by iFrame. }
         iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
-        iApply (type_type _ _ _ [ r ◁ box (uninit 1); #l +ₗ #2 ◁ &uniq{α} ty;
+        iApply (type_type _ _ _ [ r ◁ box (uninit 1); #l +ₗ #2 ◁ &uniq{α}ty;
                                   rcx ◁ box (uninit 1)]
                 with "[] LFT HE Hna HL Hk [-]"); last first.
         { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val
@@ -1041,7 +1041,7 @@ Section code.
           iLeft. iFrame. rewrite Z2Nat.inj_pos Pos2Nat.inj_succ SuccNat2Pos.id_succ //. }
         { iExists _. iFrame. }
         iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
-        iApply (type_type _ _ _ [ r ◁ box (uninit 1); #(lr +ₗ 2) ◁ &uniq{α} ty;
+        iApply (type_type _ _ _ [ r ◁ box (uninit 1); #(lr +ₗ 2) ◁ &uniq{α}ty;
                                   rcx ◁ box (uninit 1)]
                 with "[] LFT HE Hna HL Hk [-]"); last first.
         { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val
@@ -1099,7 +1099,7 @@ Section code.
         by rewrite /Z.to_nat Pos2Nat.inj_succ SuccNat2Pos.id_succ. }
       { iExists _.  iFrame. }
       iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
-      iApply (type_type _ _ _ [ #l ◁ rc ty; #l' +ₗ #2 ◁ &uniq{α} ty;
+      iApply (type_type _ _ _ [ #l ◁ rc ty; #l' +ₗ #2 ◁ &uniq{α}ty;
                                 r ◁ box (uninit 1); rcx ◁ box (uninit 1) ]
               with "[] LFT HE Hna HL Hk [-]"); last first.
       { rewrite 3!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val
diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v
index c19b24510ca1aecf17d167ad14d7106437303cff..4e50af06d3d9102ed2c852ca1cfcbfc93ae9d2c5 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -125,13 +125,13 @@ Section code.
       delete [ #1; "w" ];; return: ["r"].
 
   Lemma rc_upgrade_type ty `{!TyWf ty} :
-    typed_val rc_upgrade (fn(∀ α, ∅; &shr{α} weak ty) → option (rc ty)).
+    typed_val rc_upgrade (fn(∀ α, ∅; &shr{α}(weak ty)) → option (rc ty)).
   Proof.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>w. simpl_subst.
     iApply (type_new 2); [solve_typing..|]; iIntros (r); simpl_subst.
     iApply (type_cont [] [ϝ ⊑ₗ []]
-                      (λ _, [w ◁ box (&shr{α} weak ty); r ◁ box (option (rc ty))])) ;
+                      (λ _, [w ◁ box (&shr{α}(weak ty)); r ◁ box (option (rc ty))])) ;
       [solve_typing..| |]; last first.
     { simpl. iAlways. iIntros (k arg). inv_vec arg. simpl_subst.
       iApply type_delete; [solve_typing..|].
@@ -180,7 +180,7 @@ Section code.
         rewrite [_ â‹… _]comm frac_op' -[(_ + _)%Qp]assoc Qp_div_2. auto. }
       iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
       (* Finish up the proof. *)
-      iApply (type_type _ _ _ [ w ◁ box (&shr{α} weak ty); #lr ◁ box (uninit 2);
+      iApply (type_type _ _ _ [ w ◁ box (&shr{α}(weak ty)); #lr ◁ box (uninit 2);
                                 #l' ◁ rc ty ]
           with "[] LFT HE Hna HL Hk [-]"); last first.
       { rewrite 2!tctx_interp_cons tctx_interp_singleton tctx_hasty_val !tctx_hasty_val' //.
@@ -199,7 +199,7 @@ Section code.
       { iExists _. auto with iFrame. }
       iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
       (* Finish up the proof. *)
-      iApply (type_type _ _ _ [ w ◁ box (&shr{α} weak ty); #lr ◁ box (uninit 2) ]
+      iApply (type_type _ _ _ [ w ◁ box (&shr{α}(weak ty)); #lr ◁ box (uninit 2) ]
           with "[] LFT HE Hna HL Hk [-]"); last first.
       { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
         unlock. iFrame. iExists [_;_].
@@ -215,7 +215,7 @@ Section code.
       { iExists _. auto with iFrame. }
       iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
       (* Finish up the proof. *)
-      iApply (type_type _ _ _ [ w ◁ box (&shr{α} weak ty); #lr ◁ box (uninit 2) ]
+      iApply (type_type _ _ _ [ w ◁ box (&shr{α}(weak ty)); #lr ◁ box (uninit 2) ]
           with "[] LFT HE Hna HL Hk [-]"); last first.
       { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
         unlock. iFrame. iExists [_;_].
@@ -235,7 +235,7 @@ Section code.
       delete [ #1; "rc" ];; return: ["r"].
 
   Lemma rc_downgrade_type ty `{!TyWf ty} :
-    typed_val rc_downgrade (fn(∀ α, ∅; &shr{α} rc ty) → weak ty).
+    typed_val rc_downgrade (fn(∀ α, ∅; &shr{α}(rc ty)) → weak ty).
   Proof.
     (* TODO : this is almost identical to rc_clone *)
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
@@ -276,7 +276,7 @@ Section code.
     { iExists _. iFrame "Hrc●". iExists _. rewrite /Z.add Pos.add_1_r. iFrame. }
     iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
     (* Finish up the proof. *)
-    iApply (type_type _ _ _ [ x ◁ box (&shr{α} rc ty); #lr ◁ box (weak ty)]
+    iApply (type_type _ _ _ [ x ◁ box (&shr{α}(rc ty)); #lr ◁ box (weak ty)]
         with "[] LFT HE Hna HL Hk [-]"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
       unlock. iFrame "Hx". iFrame "Hr†". iExists [# #l'].
@@ -297,7 +297,7 @@ Section code.
       delete [ #1; "w" ];; return: ["r"].
 
   Lemma weak_clone_type ty `{!TyWf ty} :
-    typed_val weak_clone (fn(∀ α, ∅; &shr{α} weak ty) → weak ty).
+    typed_val weak_clone (fn(∀ α, ∅; &shr{α}(weak ty)) → weak ty).
   Proof.
     (* TODO : this is almost identical to rc_clone *)
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
@@ -349,7 +349,7 @@ Section code.
     iMod ("Hclose2" with "Hwv") as "(Hna & Hα1 & Hwtok)".
     iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL". wp_write.
     (* Finish up the proof. *)
-    iApply (type_type _ _ _ [ x ◁ box (&shr{α} weak ty); #lr ◁ box (weak ty)]
+    iApply (type_type _ _ _ [ x ◁ box (&shr{α}(weak ty)); #lr ◁ box (weak ty)]
         with "[] LFT HE Hna HL Hk [-]"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
       unlock. iFrame. iExists [# #l']. rewrite heap_mapsto_vec_singleton /=.
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index 73165f27efc16d321a6a07907a29ea21784b97b2..87012a873bb7fa74f639dc196f6e91b4d0766d1f 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -99,7 +99,7 @@ Section ref_functions.
     iMod ("Hcloseβ" with "Hδ") as "Hβ". iMod ("Hcloseα1" with "[$H↦]") as "Hα2".
     iMod ("Hclose'" with "[$Hα1 $Hα2] HL") as "HL". iMod ("Hclose" with "Hβ HL") as "HL".
     iApply (type_type _ _ _
-           [ x ◁ box (&shr{α} ref β ty); #lr ◁ box(ref β ty)]
+           [ x ◁ box (&shr{α}(ref β ty)); #lr ◁ box(ref β ty)]
         with "[] LFT HE Hna HL Hk"); first last.
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
       rewrite /= freeable_sz_full. iFrame. iExists _. iFrame. iExists _, _, _, _, _.
diff --git a/theories/typing/lib/refcell/refcell_code.v b/theories/typing/lib/refcell/refcell_code.v
index cf20a8c7df8c6143b7dd7bb8787b1fb5e1101a54..9f1f4b40f4c5aef8589cf21b09b9082ee9db68b9 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -144,7 +144,7 @@ Section refcell_functions.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
-    iApply (type_cont [] [ϝ ⊑ₗ []] (λ _, [x ◁ box (&shr{α} refcell ty);
+    iApply (type_cont [] [ϝ ⊑ₗ []] (λ _, [x ◁ box (&shr{α}(refcell ty));
                                          r ◁ box (option (ref α ty))]));
       [iIntros (k)|iIntros "/= !#"; iIntros (k arg); inv_vec arg]; simpl_subst; last first.
     { iApply type_delete; [solve_typing..|].
@@ -251,7 +251,7 @@ Section refcell_functions.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
-    iApply (type_cont [] [ϝ ⊑ₗ []] (λ _, [x ◁ box (&shr{α} refcell ty);
+    iApply (type_cont [] [ϝ ⊑ₗ []] (λ _, [x ◁ box (&shr{α}(refcell ty));
                                             r ◁ box (option (refmut α ty))]));
       [iIntros (k)|iIntros "/= !#"; iIntros (k arg); inv_vec arg];
       simpl_subst; last first.
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index a97ecbc0d18b5cf8cdb0955af56e094a2715d550..50415055395e6c7abad309b74527c52cc1f126b4 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -145,7 +145,7 @@ Section rwlock_functions.
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
     iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
-    iApply (type_cont [] [ϝ ⊑ₗ []] (λ _, [x ◁ box (&shr{α} rwlock ty);
+    iApply (type_cont [] [ϝ ⊑ₗ []] (λ _, [x ◁ box (&shr{α}(rwlock ty));
                                             r ◁ box (option (rwlockreadguard α ty))]));
       [iIntros (k)|iIntros "/= !#"; iIntros (k arg); inv_vec arg];
       simpl_subst; last first.
@@ -257,7 +257,7 @@ Section rwlock_functions.
   Proof.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
-    iApply (type_cont [_] [ϝ ⊑ₗ []] (λ r, [x ◁ box (&shr{α} rwlock ty);
+    iApply (type_cont [_] [ϝ ⊑ₗ []] (λ r, [x ◁ box (&shr{α}(rwlock ty));
                                         r!!!0 ◁ box (option (rwlockwriteguard α ty))]));
       [iIntros (k)|iIntros "/= !#"; iIntros (k arg); inv_vec arg=>r];
       simpl_subst; last first.
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index 0450bc94121b38f470c1bd258a11719cc4ccae5d..5e3905c02b1e40ffe984b2579285943403b53631 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -20,7 +20,7 @@ Section rwlockreadguard_functions.
 
   Lemma rwlockreadguard_deref_type ty `{!TyWf ty} :
     typed_val rwlockreadguard_deref
-      (fn(∀ '(α, β), ∅; &shr{α} rwlockreadguard β ty) → &shr{α} ty).
+      (fn(∀ '(α, β), ∅; &shr{α}(rwlockreadguard β ty)) → &shr{α} ty).
   Proof.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([α β] ϝ ret arg). inv_vec arg=>x. simpl_subst.
@@ -34,7 +34,7 @@ Section rwlockreadguard_functions.
     rewrite heap_mapsto_vec_singleton. wp_read. wp_op. wp_let.
     iMod ("Hcloseα" with "[$H↦]") 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{α} rwlockreadguard β ty);
+    iApply (type_type _ _ _ [ x ◁ box (&shr{α}(rwlockreadguard β ty));
                               #(l' +ₗ 1) ◁ &shr{α}ty]
       with "[] LFT HE Hna HL Hk"); first last.
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard_code.v b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
index 4b6bd11f5d4b39a5ecfef64850009b970801f93b..548fe054bf5a19e9073dcf9fdbbc0ea22c17f6ca 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
@@ -20,7 +20,7 @@ Section rwlockwriteguard_functions.
 
   Lemma rwlockwriteguard_deref_type ty `{!TyWf ty} :
     typed_val rwlockwriteguard_deref
-      (fn(∀ '(α, β), ∅; &shr{α} rwlockwriteguard β ty) → &shr{α} ty).
+      (fn(∀ '(α, β), ∅; &shr{α}(rwlockwriteguard β ty)) → &shr{α} ty).
   Proof.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([α β] ϝ ret arg). inv_vec arg=>x. simpl_subst.
@@ -43,7 +43,7 @@ Section rwlockwriteguard_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{α} rwlockwriteguard β ty);
+    iApply (type_type _ _ _ [ x ◁ box (&shr{α}(rwlockwriteguard β ty));
                               #(l' +ₗ 1) ◁ &shr{α}ty]
             with "[] LFT HE Hna HL Hk"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
@@ -64,7 +64,7 @@ Section rwlockwriteguard_functions.
 
   Lemma rwlockwriteguard_derefmut_type ty `{!TyWf ty} :
     typed_val rwlockwriteguard_derefmut
-      (fn(∀ '(α, β), ∅; &uniq{α} rwlockwriteguard β ty) → &uniq{α} ty).
+      (fn(∀ '(α, β), ∅; &uniq{α}(rwlockwriteguard β ty)) → &uniq{α}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/product_split.v b/theories/typing/product_split.v
index 3d1a4eb29e9fed14c33b7b17dff64c5368115b76..525c039cd1d73a3dd84550cb50ad670556d2b45e 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -139,7 +139,7 @@ Section product_split.
 
   (** Unique borrows *)
   Lemma tctx_split_uniq_prod2 E L p κ ty1 ty2 :
-    tctx_incl E L [p ◁ &uniq{κ} product2 ty1 ty2]
+    tctx_incl E L [p ◁ &uniq{κ}(product2 ty1 ty2)]
                   [p ◁ &uniq{κ} ty1; p +ₗ #ty1.(ty_size) ◁ &uniq{κ} ty2].
   Proof.
     iIntros (tid q) "#LFT _ $ H".
@@ -152,7 +152,7 @@ Section product_split.
 
   Lemma tctx_merge_uniq_prod2 E L p κ ty1 ty2 :
     tctx_incl E L [p ◁ &uniq{κ} ty1; p +ₗ #ty1.(ty_size) ◁ &uniq{κ} ty2]
-                  [p ◁ &uniq{κ} product2 ty1 ty2].
+                  [p ◁ &uniq{κ}(product2 ty1 ty2)].
   Proof.
     iIntros (tid q) "#LFT _ $ H".
     rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
@@ -163,11 +163,11 @@ Section product_split.
   Qed.
 
   Lemma uniq_is_ptr κ ty tid (vl : list val) :
-    ty_own (&uniq{κ} ty) tid vl -∗ ⌜∃ l : loc, vl = [(#l) : val]⌝.
+    ty_own (&uniq{κ}ty) tid vl -∗ ⌜∃ l : loc, vl = [(#l) : val]⌝.
   Proof. iIntros "H". destruct vl as [|[[]|][]]; eauto. Qed.
 
   Lemma tctx_split_uniq_prod E L κ tyl p :
-    tctx_incl E L [p ◁ &uniq{κ} product tyl]
+    tctx_incl E L [p ◁ &uniq{κ}(product tyl)]
                   (hasty_ptr_offsets p (uniq_bor κ) tyl 0).
   Proof.
     apply tctx_split_ptr_prod.
@@ -178,7 +178,7 @@ Section product_split.
   Lemma tctx_merge_uniq_prod E L κ tyl :
     tyl ≠ [] →
     ∀ p, tctx_incl E L (hasty_ptr_offsets p (uniq_bor κ) tyl 0)
-                   [p ◁ &uniq{κ} product tyl].
+                   [p ◁ &uniq{κ}(product tyl)].
   Proof.
     intros. apply tctx_merge_ptr_prod; try done.
     - apply _.
@@ -188,7 +188,7 @@ Section product_split.
 
   (** Shared borrows *)
   Lemma tctx_split_shr_prod2 E L p κ ty1 ty2 :
-    tctx_incl E L [p ◁ &shr{κ} product2 ty1 ty2]
+    tctx_incl E L [p ◁ &shr{κ}(product2 ty1 ty2)]
                   [p ◁ &shr{κ} ty1; p +ₗ #ty1.(ty_size) ◁ &shr{κ} ty2].
   Proof.
     iIntros (tid q) "#LFT _ $ H".
@@ -200,7 +200,7 @@ Section product_split.
 
   Lemma tctx_merge_shr_prod2 E L p κ ty1 ty2 :
     tctx_incl E L [p ◁ &shr{κ} ty1; p +ₗ #ty1.(ty_size) ◁ &shr{κ} ty2]
-                  [p ◁ &shr{κ} product2 ty1 ty2].
+                  [p ◁ &shr{κ}(product2 ty1 ty2)].
   Proof.
     iIntros (tid q) "#LFT _ $ H".
     rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
@@ -214,7 +214,7 @@ Section product_split.
   Proof. iIntros "H". destruct vl as [|[[]|][]]; eauto. Qed.
 
   Lemma tctx_split_shr_prod E L κ tyl p :
-    tctx_incl E L [p ◁ &shr{κ} product tyl]
+    tctx_incl E L [p ◁ &shr{κ}(product tyl)]
                   (hasty_ptr_offsets p (shr_bor κ) tyl 0).
   Proof.
     apply tctx_split_ptr_prod.
@@ -225,7 +225,7 @@ Section product_split.
   Lemma tctx_merge_shr_prod E L κ tyl :
     tyl ≠ [] →
     ∀ p, tctx_incl E L (hasty_ptr_offsets p (shr_bor κ) tyl 0)
-                   [p ◁ &shr{κ} product tyl].
+                   [p ◁ &shr{κ}(product tyl)].
   Proof.
     intros. apply tctx_merge_ptr_prod; try done.
     - apply _.
@@ -247,14 +247,14 @@ Section product_split.
 
   Lemma tctx_extract_split_uniq_prod E L p p' κ ty tyl T T' :
     tctx_extract_hasty E L p' ty (hasty_ptr_offsets p (uniq_bor κ) tyl 0) T' →
-    tctx_extract_hasty E L p' ty ((p ◁ &uniq{κ} Π tyl) :: T) (T' ++ T).
+    tctx_extract_hasty E L p' ty ((p ◁ &uniq{κ}(Π tyl)) :: T) (T' ++ T).
   Proof.
     intros. apply (tctx_incl_frame_r T [_] (_::_)). by rewrite tctx_split_uniq_prod.
   Qed.
 
   Lemma tctx_extract_split_shr_prod E L p p' κ ty tyl T T' :
     tctx_extract_hasty E L p' ty (hasty_ptr_offsets p (shr_bor κ) tyl 0) T' →
-    tctx_extract_hasty E L p' ty ((p ◁ &shr{κ} Π tyl) :: T) ((p ◁ &shr{κ} Π tyl) :: T).
+    tctx_extract_hasty E L p' ty ((p ◁ &shr{κ}(Π tyl)) :: T) ((p ◁ &shr{κ}(Π tyl)) :: T).
   Proof.
     intros. apply (tctx_incl_frame_r _ [_] [_;_]).
     rewrite {1}copy_tctx_incl. apply (tctx_incl_frame_r _ [_] [_]).
@@ -291,13 +291,13 @@ Section product_split.
   Lemma tctx_extract_merge_uniq_prod E L p κ tyl T T' :
     tyl ≠ [] →
     extract_tyl E L p (uniq_bor κ) tyl 0 T T' →
-    tctx_extract_hasty E L p (&uniq{κ}Π tyl) T T'.
+    tctx_extract_hasty E L p (&uniq{κ}(Π tyl)) T T'.
   Proof. auto using tctx_extract_merge_ptr_prod, tctx_merge_uniq_prod. Qed.
 
   Lemma tctx_extract_merge_shr_prod E L p κ tyl T T' :
     tyl ≠ [] →
     extract_tyl E L p (shr_bor κ) tyl 0 T T' →
-    tctx_extract_hasty E L p (&shr{κ}Π tyl) T T'.
+    tctx_extract_hasty E L p (&shr{κ}(Π tyl)) T T'.
   Proof. auto using tctx_extract_merge_ptr_prod, tctx_merge_shr_prod. Qed.
 End product_split.
 
diff --git a/theories/typing/shr_bor.v b/theories/typing/shr_bor.v
index 66e76ea8403a3802e82b5455a46b61ebf915a0f5..523c005d4786c686d0bcb8a608465dcb4f1ed107 100644
--- a/theories/typing/shr_bor.v
+++ b/theories/typing/shr_bor.v
@@ -51,18 +51,17 @@ Section shr_bor.
   Proof. by iIntros (Hsync tid1 tid2 [|[[]|][]]) "H"; try iApply Hsync. Qed.
 End shr_bor.
 
-Notation "&shr{ κ } ty" := (shr_bor κ ty)
-  (format "&shr{ κ }  ty", at level 20, right associativity) : lrust_type_scope.
+Notation "&shr{ κ }" := (shr_bor κ) (format "&shr{ κ }") : lrust_type_scope.
 
 Section typing.
   Context `{typeG Σ}.
 
   Lemma shr_mono' E L κ1 κ2 ty1 ty2 :
     lctx_lft_incl E L κ2 κ1 → subtype E L ty1 ty2 →
-    subtype E L (&shr{κ1} ty1) (&shr{κ2} ty2).
+    subtype E L (&shr{κ1}ty1) (&shr{κ2}ty2).
   Proof. by intros; apply shr_mono. Qed.
   Lemma shr_proper' E L κ ty1 ty2 :
-    eqtype E L ty1 ty2 → eqtype E L (&shr{κ} ty1) (&shr{κ} ty2).
+    eqtype E L ty1 ty2 → eqtype E L (&shr{κ}ty1) (&shr{κ}ty2).
   Proof. by intros; apply shr_proper. Qed.
 
   Lemma tctx_reborrow_shr E L p ty κ κ' :
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index e01d100faf71919ba28b70e81fe339dbe4d24627..35867764cea5cdd1b38bf8f026e764365a0fdb6f 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -58,8 +58,8 @@ Section case.
     lctx_lft_alive E L κ →
     Forall2 (λ ty e,
       typed_body E L C ((p +ₗ #1 ◁ &uniq{κ}ty) :: T) e ∨
-      typed_body E L C ((p ◁ &uniq{κ}sum tyl) :: T) e) tyl el →
-    typed_body E L C ((p ◁ &uniq{κ}sum tyl) :: T) (case: !p of el).
+      typed_body E L C ((p ◁ &uniq{κ}(sum tyl)) :: T) e) tyl el →
+    typed_body E L C ((p ◁ &uniq{κ}(sum tyl)) :: T) (case: !p of el).
   Proof.
     iIntros (Halive Hel tid) "#LFT #HE Hna HL HC HT". wp_bind p.
     rewrite tctx_interp_cons. iDestruct "HT" as "[Hp HT]".
@@ -99,11 +99,11 @@ Section case.
   Qed.
 
   Lemma type_case_uniq E L C T T' p κ tyl el :
-    tctx_extract_hasty E L p (&uniq{κ}sum tyl) T T' →
+    tctx_extract_hasty E L p (&uniq{κ}(sum tyl)) T T' →
     lctx_lft_alive E L κ →
     Forall2 (λ ty e,
       typed_body E L C ((p +ₗ #1 ◁ &uniq{κ}ty) :: T') e ∨
-      typed_body E L C ((p ◁ &uniq{κ}sum tyl) :: T') e) tyl el →
+      typed_body E L C ((p ◁ &uniq{κ}(sum tyl)) :: T') e) tyl el →
     typed_body E L C T (case: !p of el).
   Proof. unfold tctx_extract_hasty=>->. apply type_case_uniq'. Qed.
 
@@ -111,8 +111,8 @@ Section case.
     lctx_lft_alive E L κ →
     Forall2 (λ ty e,
       typed_body E L C ((p +ₗ #1 ◁ &shr{κ}ty) :: T) e ∨
-      typed_body E L C ((p ◁ &shr{κ}sum tyl) :: T) e) tyl el →
-    typed_body E L C ((p ◁ &shr{κ}sum tyl) :: T) (case: !p of el).
+      typed_body E L C ((p ◁ &shr{κ}(sum tyl)) :: T) e) tyl el →
+    typed_body E L C ((p ◁ &shr{κ}(sum tyl)) :: T) (case: !p of el).
   Proof.
     iIntros (Halive Hel tid) "#LFT #HE Hna HL HC HT". wp_bind p.
     rewrite tctx_interp_cons. iDestruct "HT" as "[Hp HT]".
@@ -132,7 +132,7 @@ Section case.
   Qed.
 
   Lemma type_case_shr E L C T p κ tyl el :
-    p ◁ &shr{κ}sum tyl ∈ T →
+    p ◁ &shr{κ}(sum tyl) ∈ T →
     lctx_lft_alive E L κ →
     Forall2 (λ ty e, typed_body E L C ((p +ₗ #1 ◁ &shr{κ}ty) :: T) e) tyl el →
     typed_body E L C T (case: !p of el).
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index c0fca1b285ccd6b08ffd823e8974830c77b1f773..baafe6bacb95cfc6bace8ff198720d1c357fa8da 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -96,18 +96,17 @@ Section uniq_bor.
   Qed.
 End uniq_bor.
 
-Notation "&uniq{ κ } ty" := (uniq_bor κ ty)
-  (format "&uniq{ κ }  ty", at level 20, right associativity) : lrust_type_scope.
+Notation "&uniq{ κ }" := (uniq_bor κ) (format "&uniq{ κ }") : lrust_type_scope.
 
 Section typing.
   Context `{typeG Σ}.
 
   Lemma uniq_mono' E L κ1 κ2 ty1 ty2 :
     lctx_lft_incl E L κ2 κ1 → eqtype E L ty1 ty2 →
-    subtype E L (&uniq{κ1} ty1) (&uniq{κ2} ty2).
+    subtype E L (&uniq{κ1}ty1) (&uniq{κ2}ty2).
   Proof. by intros; apply uniq_mono. Qed.
   Lemma uniq_proper' E L κ ty1 ty2 :
-    eqtype E L ty1 ty2 → eqtype E L (&uniq{κ} ty1) (&uniq{κ} ty2).
+    eqtype E L ty1 ty2 → eqtype E L (&uniq{κ}ty1) (&uniq{κ}ty2).
   Proof. by intros; apply uniq_proper. Qed.
 
   Lemma tctx_share E L p κ ty :