From 026f759e6e547f363e9a7b8289fc7b876e786e41 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 28 Mar 2017 13:59:34 +0200
Subject: [PATCH] Remove redefined list notations in scopes.

Instead, I have added subscripts to the inclusion notations. This makes pretty
printing much more reliable, and generally even shortens things, as no scope
annotations are needed.
---
 theories/typing/bool.v                        |  2 +-
 theories/typing/cont.v                        |  2 +-
 theories/typing/cont_context.v                | 23 ++-----
 theories/typing/function.v                    | 28 ++++-----
 theories/typing/lft_contexts.v                | 62 +++++++------------
 theories/typing/lib/cell.v                    |  2 +-
 theories/typing/lib/fake_shared_box.v         |  2 +-
 theories/typing/lib/option.v                  |  2 +-
 theories/typing/lib/rc.v                      | 30 ++++-----
 theories/typing/lib/refcell/ref_code.v        | 14 ++---
 theories/typing/lib/refcell/refcell_code.v    | 22 +++----
 theories/typing/lib/refcell/refmut_code.v     | 14 ++---
 theories/typing/lib/rwlock/rwlock_code.v      | 24 +++----
 .../typing/lib/rwlock/rwlockreadguard_code.v  |  8 +--
 .../typing/lib/rwlock/rwlockwriteguard_code.v |  6 +-
 theories/typing/lib/spawn.v                   |  8 +--
 theories/typing/product_split.v               |  4 +-
 theories/typing/programs.v                    | 27 ++++----
 theories/typing/type.v                        |  2 +-
 theories/typing/type_context.v                | 29 ++-------
 theories/typing/type_sum.v                    |  8 +--
 21 files changed, 136 insertions(+), 183 deletions(-)

diff --git a/theories/typing/bool.v b/theories/typing/bool.v
index db1825ad..84dba1c6 100644
--- a/theories/typing/bool.v
+++ b/theories/typing/bool.v
@@ -38,7 +38,7 @@ Section typing.
   Proof. iIntros. iApply type_let; [apply type_bool_instr|solve_typing|done]. Qed.
 
   Lemma type_if E L C T e1 e2 p:
-    (p ◁ bool)%TC ∈ T →
+    p ◁ bool ∈ T →
     typed_body E L C T e1 -∗ typed_body E L C T e2 -∗
     typed_body E L C T (if: p then e1 else e2).
   Proof.
diff --git a/theories/typing/cont.v b/theories/typing/cont.v
index 91665210..caa9284b 100644
--- a/theories/typing/cont.v
+++ b/theories/typing/cont.v
@@ -13,7 +13,7 @@ Section typing.
          args = of_val <$> argsv, only because then solve_typing
          is able to prove it easily. *)
     Forall2 (λ a av, to_val a = Some av ∨ a = of_val av) args argsv →
-    (k ◁cont(L, T'))%CC ∈ C →
+    k ◁cont(L, T') ∈ C →
     tctx_incl E L T (T' (list_to_vec argsv)) →
     typed_body E L C T (k args).
   Proof.
diff --git a/theories/typing/cont_context.v b/theories/typing/cont_context.v
index 5d90ab31..ae290251 100644
--- a/theories/typing/cont_context.v
+++ b/theories/typing/cont_context.v
@@ -17,28 +17,18 @@ Add Printing Constructor cctx_elt.
 
 Notation cctx := (list cctx_elt).
 
-Delimit Scope lrust_cctx_scope with CC.
-Bind Scope lrust_cctx_scope with cctx_elt.
-
-Notation "k ◁cont( L , T )" := (CCtx_iscont k L%LL _ T%TC)
-  (at level 70, format "k  ◁cont( L ,  T )") : lrust_cctx_scope.
-Notation "a :: b" := (@cons cctx_elt a%CC b%CC)
-  (at level 60, right associativity) : lrust_cctx_scope.
-Notation "[ x1 ; x2 ; .. ; xn ]" :=
-  (@cons cctx_elt x1%CC (@cons cctx_elt x2%CC
-        (..(@cons cctx_elt xn%CC (@nil cctx_elt))..))) : lrust_cctx_scope.
-Notation "[ x ]" := (@cons cctx_elt x%CC (@nil cctx_elt)) : lrust_cctx_scope.
+Notation "k ◁cont( L , T )" := (CCtx_iscont k L _ T)
+  (at level 70, format "k  ◁cont( L ,  T )").
 
 Section cont_context.
   Context `{typeG Σ}.
 
   Definition cctx_elt_interp (tid : thread_id) (x : cctx_elt) : iProp Σ :=
-    let '(k ◁cont(L, T))%CC := x in
+    let '(k ◁cont(L, T)) := x in
     (∀ args, na_own tid ⊤ -∗ llctx_interp L 1 -∗ tctx_interp tid (T args) -∗
          WP k (of_val <$> (args : list _)) {{ _, cont_postcondition }})%I.
   Definition cctx_interp (tid : thread_id) (C : cctx) : iProp Σ :=
     (∀ (x : cctx_elt), ⌜x ∈ C⌝ -∗ cctx_elt_interp tid x)%I.
-  Global Arguments cctx_interp _ _%CC.
 
   Global Instance cctx_interp_permut tid:
     Proper ((≡ₚ) ==> (⊣⊢)) (cctx_interp tid).
@@ -73,12 +63,11 @@ Section cont_context.
   Proof.
     rewrite /cctx_interp. iIntros "H". iIntros ([k L n T]) "%".
     iIntros (args) "HL HT". iMod "H".
-    by iApply ("H" $! (k ◁cont(L, T)%CC) with "[%] HL HT").
+    by iApply ("H" $! (k ◁cont(L, T)) with "[%] HL HT").
   Qed.
 
   Definition cctx_incl (E : elctx) (C1 C2 : cctx): Prop :=
     ∀ tid, lft_ctx -∗ elctx_interp E -∗ cctx_interp tid C1 -∗ cctx_interp tid C2.
-  Global Arguments cctx_incl _%EL _%CC _%CC.
 
   Global Instance cctx_incl_preorder E : PreOrder (cctx_incl E).
   Proof.
@@ -102,7 +91,7 @@ Section cont_context.
     iIntros (x) "Hin". iDestruct "Hin" as %[->|Hin]%elem_of_cons.
     - iIntros (args) "Htl HL HT".
       iMod (HT1T2 with "LFT HE HL HT") as "(HL & HT)".
-      iApply ("H" $! (_ ◁cont(_, _))%CC with "[%] Htl HL HT").
+      iApply ("H" $! (_ ◁cont(_, _)) with "[%] Htl HL HT").
       constructor.
     - iApply (HC1C2 with "LFT HE [H] [%]"); last done.
       iIntros (x') "%". iApply ("H" with "[%]"). by apply elem_of_cons; auto.
@@ -112,7 +101,7 @@ Section cont_context.
   Proof. apply incl_cctx_incl. by set_unfold. Qed.
 
   Lemma cctx_incl_cons E k L n (T1 T2 : vec val n → tctx) C1 C2 :
-    (k ◁cont(L, T1))%CC ∈ C1 →
+    k ◁cont(L, T1) ∈ C1 →
     (∀ args, tctx_incl E L (T2 args) (T1 args)) →
     cctx_incl E C1 C2 →
     cctx_incl E C1 (k ◁cont(L, T2) :: C2).
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 1f413f86..eed35718 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -19,8 +19,8 @@ Section fn.
     {| st_own tid vl := (∃ fb kb xb e H,
          ⌜vl = [@RecV fb (kb::xb) e H]⌝ ∗ ⌜length xb = n⌝ ∗
          ▷ ∀ (x : A) (ϝ : lft) (k : val) (xl : vec val (length xb)),
-            □ typed_body ((fp x).(fp_E)  ϝ) [ϝ ⊑ []]
-                         [k◁cont([ϝ ⊑ []], λ v : vec _ 1, [v!!!0 ◁ box (fp x).(fp_ty)])]
+            □ typed_body ((fp x).(fp_E)  ϝ) [ϝ ⊑ₗ []]
+                         [k◁cont([ϝ ⊑ₗ []], λ v : vec _ 1, [v!!!0 ◁ box (fp x).(fp_ty)])]
                          (zip_with (TCtx_hasty ∘ of_val) xl
                                    (box <$> (vec_to_list (fp x).(fp_tys))))
                          (subst_v (fb::kb::xb) (RecV fb (kb::xb) e:::k:::xl) e))%I |}.
@@ -172,7 +172,7 @@ Section typing.
     - unfold cctx_interp. iIntros (elt) "Helt".
       iDestruct "Helt" as %->%elem_of_list_singleton. iIntros (ret) "Htl HL HT".
       unfold cctx_elt_interp.
-      iApply ("HC" $! (_ ◁cont(_, _)%CC) with "[%] Htl HL [> -]").
+      iApply ("HC" $! (_ ◁cont(_, _)) with "[%] Htl HL [> -]").
       { by apply elem_of_list_singleton. }
       rewrite /tctx_interp !big_sepL_singleton /=.
       iDestruct "HT" as (v) "[HP Hown]". iExists v. iFrame "HP".
@@ -234,7 +234,7 @@ Section typing.
   Lemma type_call' {A} E L T p (κs : list lft) (ps : list path)
                          (fp : A → fn_params (length ps)) (k : val) x :
     Forall (lctx_lft_alive E L) κs →
-    (∀ ϝ, elctx_sat (((λ κ, ϝ ⊑ κ) <$> κs)%EL ++ E) L ((fp x).(fp_E) ϝ)) →
+    (∀ ϝ, elctx_sat (((λ κ, ϝ ⊑ₑ κ) <$> κs) ++ E) L ((fp x).(fp_E) ϝ)) →
     typed_body E L [k ◁cont(L, λ v : vec _ 1, (v!!!0 ◁ box (fp x).(fp_ty)) :: T)]
                ((p ◁ fn fp) ::
                 zip_with TCtx_hasty ps (box <$> (vec_to_list (fp x).(fp_tys))) ++
@@ -286,12 +286,12 @@ Section typing.
 
   Lemma type_call {A} x E L C T T' T'' p (ps : list path)
                         (fp : A → fn_params (length ps)) k :
-    (p ◁ fn fp)%TC ∈ T →
+    p ◁ fn fp ∈ T →
     Forall (lctx_lft_alive E L) (L.*1) →
-    (∀ ϝ, elctx_sat (((λ κ, ϝ ⊑ κ) <$> (L.*1))%EL ++ E) L ((fp x).(fp_E) ϝ)) →
+    (∀ ϝ, elctx_sat (((λ κ, ϝ ⊑ₑ κ) <$> (L.*1)) ++ E) L ((fp x).(fp_E) ϝ)) →
     tctx_extract_ctx E L (zip_with TCtx_hasty ps
                                    (box <$> vec_to_list (fp x).(fp_tys))) T T' →
-    (k ◁cont(L, T''))%CC ∈ C →
+    k ◁cont(L, T'') ∈ C →
     (∀ ret : val, tctx_incl E L ((ret ◁ box (fp x).(fp_ty))::T') (T'' [# ret])) →
     typed_body E L C T (call: p ps → k).
   Proof.
@@ -306,16 +306,16 @@ Section typing.
   Lemma type_letcall {A} x E L C T T' p (ps : list path)
                         (fp : A → fn_params (length ps)) b e :
     Closed (b :b: []) e → Closed [] p → Forall (Closed []) ps →
-    (p ◁ fn fp)%TC ∈ T →
+    p ◁ fn fp ∈ T →
     Forall (lctx_lft_alive E L) (L.*1) →
-    (∀ ϝ, elctx_sat (((λ κ, ϝ ⊑ κ) <$> (L.*1))%EL ++ E) L ((fp x).(fp_E) ϝ)) →
+    (∀ ϝ, elctx_sat (((λ κ, ϝ ⊑ₑ κ) <$> (L.*1)) ++ E) L ((fp x).(fp_E) ϝ)) →
     tctx_extract_ctx E L (zip_with TCtx_hasty ps
                                    (box <$> vec_to_list (fp x).(fp_tys))) T T' →
     (∀ ret : val, typed_body E L C ((ret ◁ box (fp x).(fp_ty))::T') (subst' b ret e)) -∗
     typed_body E L C T (letcall: b := p ps in e).
   Proof.
     iIntros (?? Hpsc ????) "He".
-    iApply (type_cont_norec [_] _ (λ r, (r!!!0 ◁ box (fp x).(fp_ty)) :: T')%TC).
+    iApply (type_cont_norec [_] _ (λ r, (r!!!0 ◁ box (fp x).(fp_ty)) :: T')).
     - (* TODO : make [solve_closed] work here. *)
       eapply is_closed_weaken; first done. set_solver+.
     - (* TODO : make [solve_closed] work here. *)
@@ -344,8 +344,8 @@ Section typing.
     n = length argsb →
     Closed (fb :b: "return" :b: argsb +b+ []) e →
     □ (∀ x ϝ (f : val) k (args : vec val (length argsb)),
-          typed_body ((fp x).(fp_E) ϝ) [ϝ ⊑ []]
-                     [k ◁cont([ϝ ⊑ []], λ v : vec _ 1, [v!!!0 ◁ box (fp x).(fp_ty)])]
+          typed_body ((fp x).(fp_E) ϝ) [ϝ ⊑ₗ []]
+                     [k ◁cont([ϝ ⊑ₗ []], λ v : vec _ 1, [v!!!0 ◁ box (fp x).(fp_ty)])]
                      ((f ◁ fn fp) ::
                         zip_with (TCtx_hasty ∘ of_val) args
                                  (box <$> vec_to_list (fp x).(fp_tys)) ++ T)
@@ -369,8 +369,8 @@ Section typing.
     n = length argsb →
     Closed ("return" :b: argsb +b+ []) e →
     □ (∀ x ϝ k (args : vec val (length argsb)),
-        typed_body ((fp x).(fp_E) ϝ) [ϝ ⊑ []]
-                   [k ◁cont([ϝ ⊑ []], λ v : vec _ 1, [v!!!0 ◁ box (fp x).(fp_ty)])]
+        typed_body ((fp x).(fp_E) ϝ) [ϝ ⊑ₗ []]
+                   [k ◁cont([ϝ ⊑ₗ []], λ v : vec _ 1, [v!!!0 ◁ box (fp x).(fp_ty)])]
                    (zip_with (TCtx_hasty ∘ of_val) args
                              (box <$> vec_to_list (fp x).(fp_tys)) ++ T)
                    (subst_v (BNamed "return" :: argsb) (k ::: args) e)) -∗
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index b5359302..c3f87add 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -15,29 +15,12 @@ Delimit Scope lrust_elctx_scope with EL.
    notations, so we have to use [Arguments] everywhere. *)
 Bind Scope lrust_elctx_scope with elctx_elt.
 
-Notation "κ1 ⊑ κ2" := (@pair lft lft κ1 κ2) (at level 70) : lrust_elctx_scope.
-
-Notation "a :: b" := (@cons elctx_elt a%EL b%EL)
-  (at level 60, right associativity) : lrust_elctx_scope.
-Notation "[ x1 ; x2 ; .. ; xn ]" :=
-  (@cons elctx_elt x1%EL (@cons elctx_elt x2%EL
-        (..(@cons elctx_elt xn%EL (@nil elctx_elt))..))) : lrust_elctx_scope.
-Notation "[ x ]" := (@cons elctx_elt x%EL (@nil elctx_elt)) : lrust_elctx_scope.
+Notation "κ1 ⊑ₑ κ2" := (@pair lft lft κ1 κ2) (at level 70).
 
 Definition llctx_elt : Type := lft * list lft.
 Notation llctx := (list llctx_elt).
 
-Delimit Scope lrust_llctx_scope with LL.
-Bind Scope lrust_llctx_scope with llctx_elt.
-
-Notation "κ ⊑ κl" := (@pair lft (list lft) κ κl) (at level 70) : lrust_llctx_scope.
-
-Notation "a :: b" := (@cons llctx_elt a%LL b%LL)
-  (at level 60, right associativity) : lrust_llctx_scope.
-Notation "[ x1 ; x2 ; .. ; xn ]" :=
-  (@cons llctx_elt x1%LL (@cons llctx_elt x2%LL
-        (..(@cons llctx_elt xn%LL (@nil llctx_elt))..))) : lrust_llctx_scope.
-Notation "[ x ]" := (@cons llctx_elt x%LL (@nil llctx_elt)) : lrust_llctx_scope.
+Notation "κ ⊑ₗ κl" := (@pair lft (list lft) κ κl) (at level 70).
 
 Section lft_contexts.
   Context `{invG Σ, lftG Σ}.
@@ -76,7 +59,7 @@ Section lft_contexts.
 
   Definition llctx_interp (L : llctx) (q : Qp) : iProp Σ :=
     ([∗ list] x ∈ L, llctx_elt_interp x q)%I.
-  Global Arguments llctx_interp _%LL _%Qp.
+  Global Arguments llctx_interp _ _%Qp.
   Global Instance llctx_interp_fractional L :
     Fractional (llctx_interp L).
   Proof. intros ??. rewrite -big_sepL_sepL. by setoid_rewrite <-fractional. Qed.
@@ -88,16 +71,15 @@ Section lft_contexts.
   Proof. intros ????? ->. by apply big_opL_permutation. Qed.
 
   Lemma lctx_equalize_lft qL κ1 κ2 `{!frac_borG Σ} :
-    lft_ctx -∗ llctx_elt_interp (κ1 ⊑ [κ2]%list) qL ={⊤}=∗
-      elctx_elt_interp (κ1 ⊑ κ2) ∗ elctx_elt_interp (κ2 ⊑ κ1).
+    lft_ctx -∗ llctx_elt_interp (κ1 ⊑ₗ [κ2]%list) qL ={⊤}=∗
+      elctx_elt_interp (κ1 ⊑ₑ κ2) ∗ elctx_elt_interp (κ2 ⊑ₑ κ1).
   Proof.
-    iIntros "#LFT Hκ". rewrite /llctx_elt_interp /=. (* TODO: Why is this unfold necessary? *)
-    iDestruct "Hκ" as (κ) "(% & Hκ & _)".
+    iIntros "#LFT". iDestruct 1 as (κ) "(% & Hκ & _)"; simplify_eq/=.
     iMod (bor_create _ κ2 (qL).[κ] with "LFT [Hκ]") as "[Hκ _]";
       first done; first by iFrame.
     iMod (bor_fracture (λ q, (qL * q).[_])%I with "LFT [Hκ]") as "#Hκ"; first done.
     { rewrite Qp_mult_1_r. done. }
-    iModIntro. subst κ1. iSplit.
+    iModIntro. iSplit.
     - iApply lft_incl_trans; iApply lft_intersect_incl_l.
     - iApply (lft_incl_glb with "[]"); first iApply (lft_incl_glb with "[]").
       + iApply lft_incl_refl.
@@ -146,7 +128,7 @@ Section lft_contexts.
   Proof. iIntros (qL) "_ !# _". iApply lft_incl_static. Qed.
 
   Lemma lctx_lft_incl_local κ κ' κs :
-    (κ ⊑ κs)%LL ∈ L → κ' ∈ κs → lctx_lft_incl κ κ'.
+    κ ⊑ₗ κs ∈ L → κ' ∈ κs → lctx_lft_incl κ κ'.
   Proof.
     iIntros (? Hκ'κs qL) "H".
     iDestruct (big_sepL_elem_of with "H") as "H"; first done.
@@ -157,17 +139,17 @@ Section lft_contexts.
   Qed.
 
   Lemma lctx_lft_incl_local' κ κ' κ'' κs :
-    (κ ⊑ κs)%LL ∈ L → κ' ∈ κs → lctx_lft_incl κ' κ'' → lctx_lft_incl κ κ''.
+    κ ⊑ₗ κs ∈ L → κ' ∈ κs → lctx_lft_incl κ' κ'' → lctx_lft_incl κ κ''.
   Proof. intros. etrans; last done. by eapply lctx_lft_incl_local. Qed.
 
-  Lemma lctx_lft_incl_external κ κ' : (κ ⊑ κ')%EL ∈ E → lctx_lft_incl κ κ'.
+  Lemma lctx_lft_incl_external κ κ' : κ ⊑ₑ κ' ∈ E → lctx_lft_incl κ κ'.
   Proof.
     iIntros (??) "_ !# #HE".
     rewrite /elctx_interp /elctx_elt_interp big_sepL_elem_of //. done.
   Qed.
 
   Lemma lctx_lft_incl_external' κ κ' κ'' :
-    (κ ⊑ κ')%EL ∈ E → lctx_lft_incl κ' κ'' → lctx_lft_incl κ κ''.
+    κ ⊑ₑ κ' ∈ E → lctx_lft_incl κ' κ'' → lctx_lft_incl κ κ''.
   Proof. intros. etrans; last done. by eapply lctx_lft_incl_external. Qed.
 
   (* Lifetime aliveness *)
@@ -196,7 +178,7 @@ Section lft_contexts.
   Qed.
 
   Lemma lctx_lft_alive_local κ κs:
-    (κ ⊑ κs)%LL ∈ L → Forall lctx_lft_alive κs → lctx_lft_alive κ.
+    κ ⊑ₗ κs ∈ L → Forall lctx_lft_alive κs → lctx_lft_alive κ.
   Proof.
     iIntros ([i HL]%elem_of_list_lookup_1 Hκs F qL ?) "#HE HL".
     iDestruct "HL" as "[HL1 HL2]". rewrite {2}/llctx_interp /llctx_elt_interp.
@@ -235,7 +217,7 @@ Section lft_contexts.
   Qed.
 
   Lemma lctx_lft_alive_external κ κ':
-    (κ ⊑ κ')%EL ∈ E → lctx_lft_alive κ → lctx_lft_alive κ'.
+    κ ⊑ₑ κ' ∈ E → lctx_lft_alive κ → lctx_lft_alive κ'.
   Proof.
     intros. by eapply lctx_lft_alive_incl, lctx_lft_incl_external.
   Qed.
@@ -244,11 +226,11 @@ Section lft_contexts.
     Forall lctx_lft_alive κs →
     ∀ (F : coPset) (qL : Qp),
       ↑lftN ⊆ F → lft_ctx -∗ elctx_interp E -∗
-         llctx_interp L qL ={F}=∗ elctx_interp ((λ κ, ϝ ⊑ κ) <$> κs)%EL ∗
+         llctx_interp L qL ={F}=∗ elctx_interp ((λ κ, ϝ ⊑ₑ κ) <$> κs) ∗
                                    ([†ϝ] ={F}=∗ llctx_interp L qL).
   Proof.
     iIntros (Hκs F qL ?) "#LFT #HE". iInduction κs as [|κ κs] "IH" forall (qL Hκs).
-    { iIntros "$ !>". rewrite /elctx_interp big_sepL_nil. auto. }
+    { iIntros "$ !>". rewrite /elctx_interp /=; auto. }
     iIntros "[HL1 HL2]". inversion Hκs as [|?? Hκ Hκs']. clear Hκs. subst.
     iMod ("IH" with "[% //] HL2") as "[#Hκs Hclose1] {IH}".
     iMod (Hκ with "HE HL1") as (q) "[Hκ Hclose2]"; first done.
@@ -270,7 +252,7 @@ Section lft_contexts.
   Proof. iIntros (?) "_ !# _". by rewrite /elctx_interp /=. Qed.
 
   Lemma elctx_sat_lft_incl E' κ κ' :
-    lctx_lft_incl κ κ' → elctx_sat E' → elctx_sat ((κ ⊑ κ') :: E')%EL.
+    lctx_lft_incl κ κ' → elctx_sat E' → elctx_sat ((κ ⊑ₑ κ') :: E').
   Proof.
     iIntros (Hκκ' HE' qL) "HL".
     iDestruct (Hκκ' with "HL") as "#Hincl".
@@ -295,12 +277,12 @@ Section lft_contexts.
   Proof. iIntros (?) "_ !# ?". done. Qed.
 End lft_contexts.
 
-Arguments lctx_lft_incl {_ _ _} _%EL _%LL _ _.
-Arguments lctx_lft_eq {_ _ _} _%EL _%LL _ _.
-Arguments lctx_lft_alive {_ _ _} _%EL _%LL _.
-Arguments elctx_sat {_ _ _} _%EL _%LL _%EL.
-Arguments lctx_lft_incl_incl {_ _ _ _%EL _%LL} _ _.
-Arguments lctx_lft_alive_tok {_ _ _ _%EL _%LL} _ _ _.
+Arguments lctx_lft_incl {_ _ _} _ _ _ _.
+Arguments lctx_lft_eq {_ _ _} _ _ _ _.
+Arguments lctx_lft_alive {_ _ _} _ _ _.
+Arguments elctx_sat {_ _ _} _ _ _.
+Arguments lctx_lft_incl_incl {_ _ _ _ _} _ _.
+Arguments lctx_lft_alive_tok {_ _ _ _ _} _ _ _.
 
 Lemma elctx_sat_submseteq `{invG Σ, lftG Σ} E E' L :
   E' ⊆+ E → elctx_sat E L E'.
diff --git a/theories/typing/lib/cell.v b/theories/typing/lib/cell.v
index 1de6c057..eff85844 100644
--- a/theories/typing/lib/cell.v
+++ b/theories/typing/lib/cell.v
@@ -181,7 +181,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]%TC
+           [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†".
diff --git a/theories/typing/lib/fake_shared_box.v b/theories/typing/lib/fake_shared_box.v
index f2523481..a641cdb3 100644
--- a/theories/typing/lib/fake_shared_box.v
+++ b/theories/typing/lib/fake_shared_box.v
@@ -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) ]%TC
+    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/option.v b/theories/typing/lib/option.v
index 9b6594b0..fa791035 100644
--- a/theories/typing/lib/option.v
+++ b/theories/typing/lib/option.v
@@ -30,7 +30,7 @@ Section option.
       inv_vec p=>o. simpl_subst.
     iApply type_deref; [solve_typing..|]. iIntros (o'). simpl_subst.
     iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
-    iApply (type_cont [] [ϝ ⊑ []]%LL (λ _, [o ◁ _; r ◁ _])%TC) ; [solve_typing..| |].
+    iApply (type_cont [] [ϝ ⊑ₗ []] (λ _, [o ◁ _; r ◁ _])) ; [solve_typing..| |].
     - iIntros (k). simpl_subst.
       iApply type_case_uniq; [solve_typing..|].
         constructor; last constructor; last constructor; left.
diff --git a/theories/typing/lib/rc.v b/theories/typing/lib/rc.v
index c3a9c6df..19de1159 100644
--- a/theories/typing/lib/rc.v
+++ b/theories/typing/lib/rc.v
@@ -274,7 +274,7 @@ Section code.
     wp_op. rewrite shift_loc_0. wp_write. wp_op. iDestruct (ty.(ty_size_eq) with "Hx") as %Hsz.
     wp_apply (wp_memcpy with "[$Hrcbox↦1 $Hx↦]"); [by auto using vec_to_list_length..|].
     iIntros "[Hrcbox↦1 Hx↦]". wp_seq. wp_op. rewrite shift_loc_0. wp_write.
-    iApply (type_type _ _ _ [ #lx ◁ box (uninit (ty_size ty)); #lrc ◁ box (rc ty)]%TC
+    iApply (type_type _ _ _ [ #lx ◁ box (uninit (ty_size ty)); #lrc ◁ box (rc ty)]
         with "[] LFT HE Hna HL Hk [-]"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //=. iFrame.
       iSplitL "Hx↦".
@@ -340,7 +340,7 @@ Section code.
       rewrite [_ â‹… _]comm frac_op' -[(_ + _)%Qp]assoc. rewrite 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); #lrc2 ◁ box (rc ty)]%TC
+    iApply (type_type _ _ _ [ x ◁ box (&shr{α} rc ty); #lrc2 ◁ 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 "Hrc2†". iExists [_]. rewrite heap_mapsto_vec_singleton.
@@ -380,7 +380,7 @@ Section code.
     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)]%TC
+    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.
@@ -414,8 +414,8 @@ Section code.
     iIntros (_ ϝ ret arg). inv_vec arg=>rcx. simpl_subst.
     iApply type_new; [solve_typing..|]; iIntros (x); simpl_subst.
     rewrite (Nat2Z.id (Σ[ ty; rc ty ]).(ty_size)).
-    iApply (type_cont [] [ϝ ⊑ []]%LL
-                      (λ _, [rcx ◁ box (uninit 1); x ◁ box (Σ[ ty; rc ty ])])%TC) ;
+    iApply (type_cont [] [ϝ ⊑ₗ []]
+                      (λ _, [rcx ◁ box (uninit 1); x ◁ box (Σ[ ty; rc ty ])])) ;
       [solve_typing..| |]; last first.
     { simpl. iAlways. iIntros (k arg). inv_vec arg. simpl_subst.
       iApply type_delete; [solve_typing..|].
@@ -433,7 +433,7 @@ Section code.
       iApply (type_type _ _ _ [ x ◁ own_ptr (ty_size Σ[ ty; rc ty ]) (uninit _);
                                 rcx ◁ box (uninit 1);
                                 #rc' +ₗ #1 ◁ own_ptr (S ty.(ty_size)) ty;
-                                #rc' +ₗ #0 ◁ own_ptr (S ty.(ty_size)) (uninit 1%nat)]%TC
+                                #rc' +ₗ #0 ◁ own_ptr (S ty.(ty_size)) (uninit 1%nat)]
         with "[] LFT HE Hna HL Hk [-]"); last first.
       { unlock. rewrite 3!tctx_interp_cons tctx_interp_singleton.
         rewrite 2!tctx_hasty_val tctx_hasty_val' // tctx_hasty_val' //.
@@ -451,7 +451,7 @@ Section code.
       wp_if. iMod ("Hclose" with "[> $Hrc● $Hrc $Hna]") as "Hna"; first by eauto.
       iApply (type_type _ _ _ [ x ◁ own_ptr (ty_size Σ[ ty; rc ty ]) (uninit _);
                                 rcx ◁ box (uninit 1);
-                                #rc' ◁ rc ty ]%TC
+                                #rc' ◁ rc ty ]
         with "[] LFT HE Hna HL Hk [-]"); last first.
       { rewrite 2!tctx_interp_cons tctx_interp_singleton.
         rewrite !tctx_hasty_val tctx_hasty_val' //. unlock. iFrame.
@@ -485,8 +485,8 @@ Section code.
     iIntros (_ ϝ ret arg). inv_vec arg=>rcx. simpl_subst.
     iApply type_new; [solve_typing..|]; iIntros (x); simpl_subst.
     rewrite (Nat2Z.id (option ty).(ty_size)).
-    iApply (type_cont [] [ϝ ⊑ []]%LL
-                      (λ _, [rcx ◁ box (uninit 1); x ◁ box (option ty)])%TC);
+    iApply (type_cont [] [ϝ ⊑ₗ []]
+                      (λ _, [rcx ◁ box (uninit 1); x ◁ box (option ty)]));
       [solve_typing..| |]; last first.
     { simpl. iAlways. iIntros (k arg). inv_vec arg. simpl_subst.
       iApply type_delete; [solve_typing..|].
@@ -505,7 +505,7 @@ Section code.
       iApply (type_type _ _ _ [ x ◁ own_ptr (ty_size (option ty)) (uninit _);
                                 rcx ◁ box (uninit 1);
                                 #rc' +ₗ #1 ◁ own_ptr (S ty.(ty_size)) ty;
-                                #rc' +ₗ #0 ◁ own_ptr (S ty.(ty_size)) (uninit 1%nat)]%TC
+                                #rc' +ₗ #0 ◁ own_ptr (S ty.(ty_size)) (uninit 1%nat)]
         with "[] LFT HE Hna HL Hk [-]"); last first.
       { unlock. rewrite 3!tctx_interp_cons tctx_interp_singleton.
         rewrite 2!tctx_hasty_val tctx_hasty_val' // tctx_hasty_val' //.
@@ -529,7 +529,7 @@ Section code.
         rewrite Pos2Z.inj_sub //. iFrame "Hrc". iRight. iExists _.
         auto with iFrame. }
       iApply (type_type _ _ _ [ x ◁ own_ptr (ty_size (option ty)) (uninit _);
-                                rcx ◁ box (uninit 1)]%TC
+                                rcx ◁ box (uninit 1)]
         with "[] LFT HE Hna HL Hk [-]"); last first.
       { rewrite tctx_interp_cons tctx_interp_singleton.
         rewrite !tctx_hasty_val. unlock. iFrame. }
@@ -559,8 +559,8 @@ Section code.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>rcx. simpl_subst.
     iApply type_new; [solve_typing..|]; iIntros (x); simpl_subst. rewrite (Nat2Z.id 2%nat).
-    iApply (type_cont [] [ϝ ⊑ []]%LL
-                      (λ r, [rcx ◁ box (uninit 1); x ◁ box (option $ &uniq{α} ty)])%TC);
+    iApply (type_cont [] [ϝ ⊑ₗ []]
+                      (λ r, [rcx ◁ box (uninit 1); x ◁ box (option $ &uniq{α} ty)]));
       [solve_typing..| |]; last first.
     { simpl. iAlways. iIntros (k arg). inv_vec arg. simpl_subst.
       iApply type_delete; [solve_typing..|].
@@ -588,7 +588,7 @@ Section code.
       iMod ("Hclose1" with "Hα HL") as "HL".
       iApply (type_type _ _ _ [ x ◁ box (uninit 2);
                                  #l +ₗ #1 ◁ &uniq{α} ty;
-                                rcx ◁ box (uninit 1)]%TC
+                                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. }
@@ -605,7 +605,7 @@ Section code.
         iRight. iExists _, _, _, _. iFrame "#∗". }
       iMod ("Hclose1" with "Hα HL") as "HL".
       iApply (type_type _ _ _ [ x ◁ box (uninit 2);
-                                rcx ◁ box (uninit 1)]%TC
+                                rcx ◁ box (uninit 1)]
         with "[] LFT HE Hna HL Hk [-]"); last first.
       { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
         unlock. iFrame. }
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index 4f65c7b1..40ff2375 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)]%TC
+           [ 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 _, _, _, _, _.
@@ -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]%TC
+        [ 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. }
@@ -194,7 +194,7 @@ Section ref_functions.
     iApply (wp_step_fupd with "INV"); [set_solver..|]. wp_seq.
     iIntros "INV !>". wp_seq. iMod ("Hcloseβ" with "[$INV] Hna") as "[Hβ Hna]".
     iMod ("Hcloseα" with "Hβ") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
-    iApply (type_type _ _ _ [ #lx ◁ box (uninit 2)]%TC with "[] LFT HE Hna HL Hk");
+    iApply (type_type _ _ _ [ #lx ◁ box (uninit 2)] with "[] LFT HE Hna HL Hk");
       first last.
     { rewrite tctx_interp_singleton tctx_hasty_val' //. iFrame. iExists [ #lv;#lrc].
       rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton uninit_own. iFrame. auto. }
@@ -243,10 +243,10 @@ Section ref_functions.
     iAssert (κ ⊑ α ⊓ ν)%I with "[>Hb]" as "#Hκν".
     { iApply (lft_incl_glb with "Hκα"). iApply (frac_bor_lft_incl with "LFT").
       iApply (bor_fracture with "LFT [> -]"); first done. rewrite /= Qp_mult_1_r //. }
-    iApply (type_type ((κ ⊑ α ⊓ ν) :: (α ⊓ ν ⊑ α) :: _)%EL _
-        [k ◁cont(_, λ x:vec val 1, [ x!!!0 ◁ box (&shr{α ⊓ ν}ty2)])]%CC
+    iApply (type_type ((κ ⊑ₑ α ⊓ ν) :: (α ⊓ ν ⊑ₑ α) :: _) _
+        [k ◁cont(_, λ x:vec val 1, [ x!!!0 ◁ box (&shr{α ⊓ ν}ty2)])]
         [ f' ◁ fn(∀ α, ∅; envty, &shr{α}ty1) → &shr{α}ty2;
-          #lx ◁ box (&shr{α ⊓ ν}ty1); env ◁ box envty ]%TC
+          #lx ◁ box (&shr{α ⊓ ν}ty1); env ◁ box envty ]
        with "[] LFT [] Hna HL [-H† Hlx Henv]"); swap 1 2; swap 3 4.
     { iSplitL; last iSplitL; [done|iApply lft_intersect_incl_l|iApply "HE"]. }
     { iApply (type_call (α ⊓ ν)); solve_typing. }
@@ -269,7 +269,7 @@ Section ref_functions.
       first by rewrite -lft_dead_or; auto. wp_seq. wp_write.
     iApply (type_type _ [_] _
         [ f ◁ box (fn(∀ α, ∅; envty, &shr{α}ty1) → &shr{α}ty2);
-          #lref ◁ box (ref α ty2) ]%TC
+          #lref ◁ box (ref α ty2) ]
        with "[] LFT HE Hna [HL] Hk"); first last.
     { iFrame. rewrite big_sepL_singleton tctx_hasty_val. iExists _. iSplit. done.
       iFrame. iExists [_;_]. rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
diff --git a/theories/typing/lib/refcell/refcell_code.v b/theories/typing/lib/refcell/refcell_code.v
index 6f986424..f633a561 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -35,7 +35,7 @@ Section refcell_functions.
     rewrite shift_loc_0. wp_write. wp_op. iDestruct (ty.(ty_size_eq) with "Hx") as %Hsz.
     wp_apply (wp_memcpy with "[$Hr↦1 $Hx↦]"); [by auto using vec_to_list_length..|].
     iIntros "[Hr↦1 Hx↦]". wp_seq.
-    iApply (type_type _ _ _ [ #lx ◁ box (uninit (ty_size ty)); #lr ◁ box (refcell ty)]%TC
+    iApply (type_type _ _ _ [ #lx ◁ box (uninit (ty_size ty)); #lr ◁ box (refcell ty)]
         with "[] LFT HE Hna HL Hk [-]"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //=. iFrame.
       iSplitL "Hx↦".
@@ -71,7 +71,7 @@ Section refcell_functions.
     iDestruct (ownptr_uninit_own with "Hr") as (lr vlr) "(% & Hr↦ & Hr†)". subst r.
     wp_op. wp_apply (wp_memcpy with "[$Hr↦ $Hx↦1]"); [by auto using vec_to_list_length..|].
     iIntros "[Hr↦ Hx↦1]". wp_seq.
-    iApply (type_type _ _ _ [ #lx ◁ box (uninit (S (ty_size ty))); #lr ◁ box ty]%TC
+    iApply (type_type _ _ _ [ #lx ◁ box (uninit (S (ty_size ty))); #lr ◁ box ty]
         with "[] LFT HE Hna HL Hk [-]"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //. iFrame.
       iSplitR "Hr↦ Hx".
@@ -110,7 +110,7 @@ Section refcell_functions.
     destruct x as [[|lx|]|]; try done. iDestruct "Hx" as "[Hx Hx†]".
     iDestruct "Hx" as (vl) "[Hx↦ Hx]". rewrite uninit_own. wp_op.
     iApply (type_type _ _ _
-            [ #lx ◁ box (uninit 1); #(shift_loc lx' 1) ◁ &uniq{α}ty]%TC
+            [ #lx ◁ box (uninit 1); #(shift_loc lx' 1) ◁ &uniq{α}ty]
             with "[] LFT HE Hna HL HC [-]"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //. iFrame.
       iNext. iExists _. rewrite uninit_own. iFrame. }
@@ -146,8 +146,8 @@ Section refcell_functions.
     intros. 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 [] [ϝ ⊑ []]%LL (λ _, [x ◁ box (&shr{α} refcell ty);
-                                         r ◁ box (option (ref α ty))])%TC);
+    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..|].
       iApply type_jump; solve_typing. }
@@ -165,7 +165,7 @@ Section refcell_functions.
       iMod ("Hclose'" with "[$Hβtok1 $Hβtok2]") as "Hα".
       iMod ("Hclose" with "Hα HL") as "HL".
       iApply (type_type _ _ _
-              [ x ◁ box (&shr{α}(refcell ty)); r ◁ box (uninit 3) ]%TC
+              [ x ◁ box (&shr{α}(refcell ty)); r ◁ box (uninit 3) ]
               with "[] LFT HE Hna HL Hk"); first last.
       { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
       iApply (type_sum_unit (option $ ref α ty)); [solve_typing..|]; first last.
@@ -213,7 +213,7 @@ Section refcell_functions.
       iMod ("Hclose'" with "[$Hβtok1 $Hβtok2]") as "Hα".
       iMod ("Hclose" with "Hα HL") as "HL".
       iApply (type_type  _ _ _
-        [ x ◁ box (&shr{α}(refcell ty)); r ◁ box (uninit 3); #lref ◁ box (ref α ty)]%TC
+        [ x ◁ box (&shr{α}(refcell ty)); r ◁ box (uninit 3); #lref ◁ box (ref α ty)]
               with "[] LFT HE Hna HL Hk"); first last.
       { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame.
         rewrite tctx_hasty_val' //. rewrite /= freeable_sz_full. iFrame.
@@ -253,8 +253,8 @@ Section refcell_functions.
     intros. 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 [] [ϝ ⊑ []]%LL (λ _, [x ◁ box (&shr{α} refcell ty);
-                                            r ◁ box (option (refmut α ty))]%TC));
+    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.
     { iApply type_delete; [solve_typing..|].
@@ -286,7 +286,7 @@ Section refcell_functions.
         iApply "Hbh". rewrite -lft_dead_or. auto. }
       iMod ("Hclose'" with "Hβtok") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
       iApply (type_type _ _ _
-        [ x ◁ box (&shr{α}(refcell ty)); r ◁ box (uninit 3); #lref ◁ box (refmut α ty)]%TC
+        [ x ◁ box (&shr{α}(refcell ty)); r ◁ box (uninit 3); #lref ◁ box (refmut α ty)]
               with "[] LFT HE Hna HL Hk"); first last.
       { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame.
         rewrite tctx_hasty_val' //. rewrite /= freeable_sz_full. iFrame.
@@ -300,7 +300,7 @@ Section refcell_functions.
         first by iExists st; iFrame.
       iMod ("Hclose'" with "Hβtok") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
       iApply (type_type _ _ _
-              [ x ◁ box (&shr{α}(refcell ty)); r ◁ box (uninit 3) ]%TC
+              [ x ◁ box (&shr{α}(refcell ty)); r ◁ box (uninit 3) ]
               with "[] LFT HE Hna HL Hk"); first last.
       { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
       iApply (type_sum_unit (option $ refmut α ty)); [solve_typing..|].
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index 0333b59c..3dd1961e 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]%TC
+    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'").
@@ -96,7 +96,7 @@ Section refmut_functions.
     wp_read. iIntros "Hb !>". 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 (uninit 1); #lv ◁ &uniq{α}ty]%TC
+    iApply (type_type _ _ _ [ x ◁ box (uninit 1); #lv ◁ &uniq{α}ty]
             with "[] LFT HE Hna HL Hk"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
       iFrame. iApply (bor_shorten with "[] Hb").
@@ -146,7 +146,7 @@ Section refmut_functions.
       apply auth_update_dealloc. rewrite -(right_id None _ (Some _)).
       apply cancel_local_update_empty, _. }
     iMod ("Hcloseα" with "Hβ") as "Hα". iMod ("Hclose" with "Hα HL") as "HL". wp_seq.
-    iApply (type_type _ _ _ [ #lx ◁ box (uninit 2)]%TC
+    iApply (type_type _ _ _ [ #lx ◁ box (uninit 2)]
             with "[] LFT HE Hna HL Hk"); last first.
     { rewrite tctx_interp_singleton tctx_hasty_val' //. iFrame. iExists [ #lv;#lrc].
       rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton uninit_own. iFrame. auto. }
@@ -196,10 +196,10 @@ Section refmut_functions.
     iAssert (κ ⊑ α ⊓ ν)%I with "[>Hb]" as "#Hκν".
     { iApply (lft_incl_glb with "Hκα"). iApply (frac_bor_lft_incl with "LFT").
       iApply (bor_fracture with "LFT [> -]"); first done. rewrite /= Qp_mult_1_r //. }
-    iApply (type_type ((κ ⊑ α ⊓ ν) :: (α ⊓ ν ⊑ α) :: _)%EL _
-        [k ◁cont(_, λ x:vec val 1, [ x!!!0 ◁ box (&uniq{α ⊓ ν}ty2)])]%CC
+    iApply (type_type ((κ ⊑ₑ α ⊓ ν) :: (α ⊓ ν ⊑ₑ α) :: _)%EL _
+        [k ◁cont(_, λ x:vec val 1, [ x!!!0 ◁ box (&uniq{α ⊓ ν}ty2)])]
         [ f' ◁ fn(∀ α, ∅; envty, &uniq{α}ty1) → &uniq{α}ty2;
-          #lx ◁ box (&uniq{α ⊓ ν}ty1); env ◁ box envty ]%TC
+          #lx ◁ box (&uniq{α ⊓ ν}ty1); env ◁ box envty ]
        with "[] LFT [] Hna HL [-H† Hlx Henv Hbor]"); swap 1 2; swap 3 4.
     { iSplitL; last iSplitL; [done|iApply lft_intersect_incl_l|iApply "HE"]. }
     { iApply (type_call (α ⊓ ν)); solve_typing. }
@@ -222,7 +222,7 @@ Section refmut_functions.
       first by rewrite -lft_dead_or; auto. wp_seq. wp_write.
     iApply (type_type _ [_] _
         [ f ◁ box (fn(∀ α, ∅; envty, &uniq{α}ty1) → &uniq{α}ty2);
-          #lref ◁ box (refmut α ty2) ]%TC
+          #lref ◁ box (refmut α ty2) ]
        with "[] LFT HE Hna [HL] Hk"); first last.
     { iFrame. rewrite big_sepL_singleton tctx_hasty_val. iExists _. iSplit. done.
       iFrame. iExists [_;_]. rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index 1298abb5..8b48334e 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -37,7 +37,7 @@ Section rwlock_functions.
     rewrite shift_loc_0. wp_write. wp_op. iDestruct (ty.(ty_size_eq) with "Hx") as %Hsz.
     wp_apply (wp_memcpy with "[$Hr↦1 $Hx↦]"); [done||lia..|].
     iIntros "[Hr↦1 Hx↦]". wp_seq.
-    iApply (type_type _ _ _ [ #lx ◁ box (uninit (ty_size ty)); #lr ◁ box (rwlock ty)]%TC
+    iApply (type_type _ _ _ [ #lx ◁ box (uninit (ty_size ty)); #lr ◁ box (rwlock ty)]
         with "[] LFT HE Hna HL Hk [-]"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //=. iFrame.
       iSplitL "Hx↦".
@@ -73,7 +73,7 @@ Section rwlock_functions.
     iDestruct "Hx" as "[% Hx]". iDestruct (ty.(ty_size_eq) with "Hx") as %Hsz.
     wp_apply (wp_memcpy with "[$Hr↦ $Hx↦1]"); [done||lia..|].
     iIntros "[Hr↦ Hx↦1]". wp_seq.
-    iApply (type_type _ _ _ [ #lx ◁ box (uninit (S (ty_size ty))); #lr ◁ box ty]%TC
+    iApply (type_type _ _ _ [ #lx ◁ box (uninit (S (ty_size ty))); #lr ◁ box ty]
         with "[] LFT HE Hna HL Hk [-]"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //. iFrame.
       iSplitR "Hr↦ Hx".
@@ -110,7 +110,7 @@ Section rwlock_functions.
     destruct x as [[|lx|]|]; try done. iDestruct "Hx" as "[Hx Hx†]".
     iDestruct "Hx" as (vl) "[Hx↦ Hx]". rewrite uninit_own. wp_op.
     iApply (type_type _ _ _
-            [ #lx ◁ box (uninit 1); #(shift_loc lx' 1) ◁ &uniq{α}ty]%TC
+            [ #lx ◁ box (uninit 1); #(shift_loc lx' 1) ◁ &uniq{α}ty]
             with "[] LFT HE Hna HL HC [-]"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //. iFrame.
       iNext. iExists _. rewrite uninit_own. iFrame. }
@@ -147,13 +147,13 @@ 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 [] [ϝ ⊑ []]%LL (λ _, [x ◁ box (&shr{α} rwlock ty);
-                                            r ◁ box (option (rwlockreadguard α ty))])%TC);
+    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.
     { iApply type_delete; [solve_typing..|].
       iApply type_jump; solve_typing. }
-    iApply (type_cont [] [ϝ ⊑ []]%LL (λ _, [x ◁ _; x' ◁ _; r ◁ _])%TC);
+    iApply (type_cont [] [ϝ ⊑ₗ []] (λ _, [x ◁ _; x' ◁ _; r ◁ _]));
       [iIntros (loop)|iIntros "/= !#"; iIntros (loop arg); inv_vec arg];
       simpl_subst.
     { iApply type_jump; solve_typing. }
@@ -171,7 +171,7 @@ Section rwlock_functions.
     iModIntro. wp_let. wp_op=>Hm1; wp_if.
     - iMod ("Hclose'" with "[$]") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
       iApply (type_type _ _ _
-              [ x ◁ box (&shr{α}(rwlock ty)); r ◁ box (uninit 2) ]%TC
+              [ x ◁ box (&shr{α}(rwlock ty)); r ◁ box (uninit 2) ]
               with "[] LFT HE Hna HL Hk"); first last.
       { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
       iApply (type_sum_unit (option $ rwlockreadguard α ty));
@@ -221,7 +221,7 @@ Section rwlock_functions.
         iMod ("Hclose'" with "[$]") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
         iApply (type_type  _ _ _
                    [ x ◁ box (&shr{α}(rwlock ty)); r ◁ box (uninit 2);
-                     #lx ◁ rwlockreadguard α ty]%TC
+                     #lx ◁ rwlockreadguard α ty]
               with "[] LFT HE Hna HL Hk"); first last.
         { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val
                   tctx_hasty_val' //. iFrame.
@@ -260,8 +260,8 @@ Section rwlock_functions.
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
-    iApply (type_cont [_] [ϝ ⊑ []]%LL (λ r, [x ◁ box (&shr{α} rwlock ty);
-                                        r!!!0 ◁ box (option (rwlockwriteguard α ty))])%TC);
+    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.
     { iApply type_delete; [solve_typing..|]. iApply type_jump; solve_typing. }
@@ -282,7 +282,7 @@ Section rwlock_functions.
       iMod ("Hclose'" with "Hβtok") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
       iModIntro. iApply (wp_if _ false). iNext.
       iApply (type_type _ _ _
-              [ x ◁ box (&shr{α}(rwlock ty)); r ◁ box (uninit 2) ]%TC
+              [ x ◁ box (&shr{α}(rwlock ty)); r ◁ box (uninit 2) ]
               with "[] LFT HE Hna HL Hk"); first last.
       { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
       iApply (type_sum_unit (option $ rwlockwriteguard α ty));
@@ -296,7 +296,7 @@ Section rwlock_functions.
       iMod ("Hclose" with "Hα HL") as "HL".
       iApply (type_type  _ _ _
                    [ x ◁ box (&shr{α}(rwlock ty)); r ◁ box (uninit 2);
-                     #lx ◁ rwlockwriteguard α ty]%TC
+                     #lx ◁ rwlockwriteguard α ty]
               with "[] LFT HE Hna HL Hk"); first last.
       { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val
                 tctx_hasty_val' //. iFrame.  iExists _, _. iFrame "∗#". }
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index e53896fc..83a178ec 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -35,7 +35,7 @@ Section rwlockreadguard_functions.
     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);
-                              #(shift_loc l' 1) ◁ &shr{α}ty]%TC
+                              #(shift_loc 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' //.
       iFrame. iApply (ty_shr_mono with "[] Hshr"). iApply lft_incl_glb; first done.
@@ -64,7 +64,7 @@ Section rwlockreadguard_functions.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
-    iApply (type_cont [] [ϝ ⊑ []]%LL (λ _, [x ◁ _; x' ◁ _])%TC);
+    iApply (type_cont [] [ϝ ⊑ₗ []] (λ _, [x ◁ _; x' ◁ _]));
       [iIntros (loop)|iIntros "/= !#"; iIntros (loop arg); inv_vec arg];
       simpl_subst.
     { iApply type_jump; solve_typing. }
@@ -124,7 +124,7 @@ Section rwlockreadguard_functions.
       iMod ("INV" with "Hlx") as "INV". iMod ("Hcloseβ" with "[$INV]") as "Hβ".
       iMod ("Hcloseα" with "Hβ") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
       iApply (wp_if _ true). iIntros "!>!>".
-      iApply (type_type _ _ _ [ x ◁ box (uninit 1)]%TC
+      iApply (type_type _ _ _ [ x ◁ box (uninit 1)]
               with "[] LFT HE Hna HL Hk"); first last.
       { rewrite tctx_interp_singleton tctx_hasty_val //. }
       iApply type_delete; [solve_typing..|].
@@ -134,7 +134,7 @@ Section rwlockreadguard_functions.
       iMod ("Hcloseβ" with "[Hlx H● Hst]") as "Hβ". by iExists _; iFrame.
       iMod ("Hcloseα" with "Hβ") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
       iApply (wp_if _ false). iIntros "!> !>".
-      iApply (type_type _ _ _ [ x ◁ box (uninit 1); #lx' ◁ rwlockreadguard α ty]%TC
+      iApply (type_type _ _ _ [ x ◁ box (uninit 1); #lx' ◁ rwlockreadguard α ty]
               with "[] LFT HE Hna HL Hk"); first last.
       { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val
                 tctx_hasty_val' //=. auto 10 with iFrame. }
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard_code.v b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
index 7ccd5321..a31256ba 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
@@ -44,7 +44,7 @@ Section rwlockwriteguard_functions.
     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);
-                              #(shift_loc l' 1) ◁ &shr{α}ty]%TC
+                              #(shift_loc 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' //.
       iFrame. iApply (ty_shr_mono with "[] Hshr'"). iApply lft_incl_glb; first done.
@@ -89,7 +89,7 @@ Section rwlockwriteguard_functions.
     wp_read. iIntros "Hb !>". 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 (uninit 1); #(shift_loc l 1) ◁ &uniq{α}ty]%TC
+    iApply (type_type _ _ _ [ x ◁ box (uninit 1); #(shift_loc l 1) ◁ &uniq{α}ty]
             with "[] LFT HE Hna HL Hk"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
       iFrame. iApply (bor_shorten with "[] Hb"). iApply lft_incl_glb.
@@ -135,7 +135,7 @@ Section rwlockwriteguard_functions.
       apply cancel_local_update_empty, _. }
     iModIntro. wp_seq. iMod ("Hcloseα" with "Hβ") as "Hα".
     iMod ("Hclose" with "Hα HL") as "HL".
-    iApply (type_type _ _ _ [ x ◁ box (uninit 1)]%TC
+    iApply (type_type _ _ _ [ x ◁ box (uninit 1)]
             with "[] LFT HE Hna HL Hk"); first last.
     { rewrite tctx_interp_singleton tctx_hasty_val //. }
     iApply type_delete; [solve_typing..|].
diff --git a/theories/typing/lib/spawn.v b/theories/typing/lib/spawn.v
index d0f1050f..d4b5bc8d 100644
--- a/theories/typing/lib/spawn.v
+++ b/theories/typing/lib/spawn.v
@@ -78,8 +78,8 @@ Section spawn.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (_ ϝ ret arg). inv_vec arg=>f env. simpl_subst.
     iApply type_deref; [solve_typing..|]. iIntros (f'). simpl_subst.
-    iApply (type_let _ _ _ _ ([f' ◁ _; env ◁ _]%TC)
-                     (λ j, [j ◁ join_handle retty]%TC)); try solve_typing; [|].
+    iApply (type_let _ _ _ _ ([f' ◁ _; env ◁ _])
+                     (λ j, [j ◁ join_handle retty])); try solve_typing; [|].
     { (* The core of the proof: showing that spawn is safe. *)
       iIntros (tid) "#LFT #HE $ $ [Hf' [Henv _]]".
       iApply (spawn_spec _ (join_inv tid retty) with "[-]");
@@ -123,8 +123,8 @@ Section spawn.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (_ ϝ ret arg). inv_vec arg=>c. simpl_subst.
     iApply type_deref; [solve_typing..|]. iIntros (c'); simpl_subst.
-    iApply (type_let _ _ _ _ ([c' ◁ _]%TC)
-                             (λ r, [r ◁ box retty]%TC)); try solve_typing; [|].
+    iApply (type_let _ _ _ _ ([c' ◁ _])
+                             (λ r, [r ◁ box retty])); try solve_typing; [|].
     { iIntros (tid) "#LFT _ $ $".
       rewrite tctx_interp_singleton tctx_hasty_val. iIntros "Hc'".
       destruct c' as [[|c'|]|]; try done. iDestruct "Hc'" as (ty') "[#Hsub Hc']".
diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index d2ca80bc..3d1a4eb2 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -13,7 +13,7 @@ Section product_split.
     match tyl with
     | [] => []
     | ty :: tyl =>
-      (p +ₗ #off ◁ ptr ty)%TC :: hasty_ptr_offsets p ptr tyl (off + ty.(ty_size))
+      (p +ₗ #off ◁ ptr ty) :: hasty_ptr_offsets p ptr tyl (off + ty.(ty_size))
     end.
 
   Lemma hasty_ptr_offsets_offset (l : loc) p (off1 off2 : nat) ptr tyl tid :
@@ -258,7 +258,7 @@ Section product_split.
   Proof.
     intros. apply (tctx_incl_frame_r _ [_] [_;_]).
     rewrite {1}copy_tctx_incl. apply (tctx_incl_frame_r _ [_] [_]).
-    rewrite tctx_split_shr_prod -(contains_tctx_incl _ _ [p' ◁ ty]%TC) //.
+    rewrite tctx_split_shr_prod -(contains_tctx_incl _ _ [p' ◁ ty]) //.
     apply submseteq_skip, submseteq_nil_l.
   Qed.
 
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index 090e8cc5..c88f822e 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -13,7 +13,7 @@ Section typing.
     (∀ tid, lft_ctx -∗ elctx_interp E -∗ na_own tid ⊤ -∗ llctx_interp L 1 -∗
                cctx_interp tid C -∗ tctx_interp tid T -∗
                WP e {{ _, cont_postcondition }})%I.
-  Global Arguments typed_body _%EL _%LL _%CC _%TC _%E.
+  Global Arguments typed_body _ _ _ _ _%E.
 
   Global Instance typed_body_llctx_permut E :
     Proper ((≡ₚ) ==> eq ==> eq ==> eq ==> (⊢)) (typed_body E).
@@ -52,7 +52,7 @@ Section typing.
               llctx_interp L 1 -∗ tctx_interp tid T1 -∗
               WP e {{ v, na_own tid ⊤ ∗
                          llctx_interp L 1 ∗ tctx_interp tid (T2 v) }})%I.
-  Global Arguments typed_instruction _%EL _%LL _%TC _%E _%TC.
+  Global Arguments typed_instruction _ _ _ _%E _.
 
   (** Writing and Reading **)
   Definition typed_write (E : elctx) (L : llctx) (ty1 ty ty2 : type) : iProp Σ :=
@@ -61,7 +61,7 @@ Section typing.
         ∃ (l : loc) vl, ⌜length vl = ty.(ty_size) ∧ v = #l⌝ ∗ l ↦∗ vl ∗
           (▷ l ↦∗: ty.(ty_own) tid ={F}=∗
             llctx_interp L qL ∗ ty2.(ty_own) tid [v]))%I.
-  Global Arguments typed_write _%EL _%LL _%T _%T _%T.
+  Global Arguments typed_write _ _ _%T _%T _%T.
 
   (* Technically speaking, we could remvoe the vl quantifiaction here and use
      mapsto_pred instead (i.e., l ↦∗: ty.(ty_own) tid). However, that would
@@ -69,17 +69,17 @@ Section typing.
      that nobody could possibly have changed the vl (because only half the
      fraction was given). So we go with the definition that is easier to prove. *)
   Definition typed_read (E : elctx) (L : llctx) (ty1 ty ty2 : type) : iProp Σ :=
-    (□ ∀ v tid F qL, ⌜lftE ∪ (↑lrustN) ⊆ F⌝ →
+    (□ ∀ v tid F qL, ⌜lftE ∪ ↑lrustN ⊆ F⌝ →
       lft_ctx -∗ elctx_interp E -∗ na_own tid F -∗
       llctx_interp L qL -∗ ty1.(ty_own) tid [v] ={F}=∗
         ∃ (l : loc) vl q, ⌜v = #l⌝ ∗ l ↦∗{q} vl ∗ ▷ ty.(ty_own) tid vl ∗
               (l ↦∗{q} vl ={F}=∗ na_own tid F ∗
                               llctx_interp L qL ∗ ty2.(ty_own) tid [v]))%I.
-  Global Arguments typed_read _%EL _%LL _%T _%T _%T.
+  Global Arguments typed_read _ _ _%T _%T _%T.
 End typing.
 
 Notation typed_instruction_ty E L T e ty :=
-  (typed_instruction E L T e (λ v : val, [v ◁ ty%list%T]%TC)).
+  (typed_instruction E L T e (λ v : val, [v ◁ ty%list%T])).
 
 Notation typed_val v ty := (∀ E L, typed_instruction_ty E L [] (of_val v) ty).
 
@@ -92,12 +92,11 @@ Section typing_rules.
     typed_body E L C T e -∗ typed_body E L C T e.
   Proof. done. Qed.
 
-  (* TODO: notation scopes need tuing to avoid the %list here. *)
   (* TODO: Proof a version of this that substitutes into a compatible context...
      if we really want to do that. *)
   Lemma type_equivalize_lft E L C T κ1 κ2 e :
-    typed_body ((κ1 ⊑ κ2) :: (κ2 ⊑ κ1) :: E) L C T e →
-    typed_body E ((κ1 ⊑ [κ2]%list) :: L) C T e.
+    typed_body ((κ1 ⊑ₑ κ2) :: (κ2 ⊑ₑ κ1) :: E) L C T e →
+    typed_body E ((κ1 ⊑ₗ [κ2]) :: L) C T e.
   Proof.
     iIntros (He tid) "#LFT #HE Htl [Hκ HL] HC HT".
     iMod (lctx_equalize_lft with "LFT Hκ") as "[Hκ1 Hκ2]".
@@ -145,7 +144,7 @@ Section typing_rules.
 
   Lemma type_newlft {E L C T} κs e :
     Closed [] e →
-    (∀ κ, typed_body E ((κ ⊑ κs) :: L) C T e) -∗
+    (∀ κ, typed_body E ((κ ⊑ₗ κs) :: L) C T e) -∗
     typed_body E L C T (Newlft ;; e).
   Proof.
     iIntros (Hc) "He". iIntros (tid) "#LFT #HE Htl HL HC HT".
@@ -160,7 +159,7 @@ Section typing_rules.
      Right now, we could take two. *)
   Lemma type_endlft E L C T1 T2 κ κs e :
     Closed [] e → UnblockTctx κ T1 T2 →
-    typed_body E L C T2 e -∗ typed_body E ((κ ⊑ κs) :: L) C T1 (Endlft ;; e).
+    typed_body E L C T2 e -∗ typed_body E ((κ ⊑ₗ κs) :: L) C T1 (Endlft ;; e).
   Proof.
     iIntros (Hc Hub) "He". iIntros (tid) "#LFT #HE Htl [Hκ HL] HC HT".
     iDestruct "Hκ" as (Λ) "(% & Htok & #Hend)".
@@ -188,7 +187,7 @@ Section typing_rules.
 
   Lemma type_assign_instr {E L} ty ty1 ty1' p1 p2 :
     typed_write E L ty1 ty ty1' →
-    typed_instruction E L [p1 ◁ ty1; p2 ◁ ty] (p1 <- p2) (λ _, [p1 ◁ ty1']%TC).
+    typed_instruction E L [p1 ◁ ty1; p2 ◁ ty] (p1 <- p2) (λ _, [p1 ◁ ty1']).
   Proof.
     iIntros (Hwrt tid) "#LFT #HE $ HL".
     rewrite tctx_interp_cons tctx_interp_singleton. iIntros "[Hp1 Hp2]".
@@ -214,7 +213,7 @@ Section typing_rules.
 
   Lemma type_deref_instr {E L} ty ty1 ty1' p :
     ty.(ty_size) = 1%nat → typed_read E L ty1 ty ty1' →
-    typed_instruction E L [p ◁ ty1] (!p) (λ v, [p ◁ ty1'; v ◁ ty]%TC).
+    typed_instruction E L [p ◁ ty1] (!p) (λ v, [p ◁ ty1'; v ◁ ty]).
   Proof.
     iIntros (Hsz Hread tid) "#LFT #HE Htl HL Hp".
     rewrite tctx_interp_singleton. wp_bind p. iApply (wp_hasty with "Hp").
@@ -267,7 +266,7 @@ Section typing_rules.
     Z.of_nat (ty.(ty_size)) = n →
     typed_write E L ty1 ty ty1' → typed_read E L ty2 ty ty2' →
     typed_instruction E L [p1 ◁ ty1; p2 ◁ ty2] (p1 <-{n} !p2)
-                      (λ _, [p1 ◁ ty1'; p2 ◁ ty2']%TC).
+                      (λ _, [p1 ◁ ty1'; p2 ◁ ty2']).
   Proof.
     iIntros (Hsz Hwrt Hread tid) "#LFT #HE Htl HL HT".
     iApply (type_memcpy_iris with "[] [] [$LFT $Htl $HE $HL HT]"); try done.
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 946c9486..35739db0 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -58,7 +58,7 @@ Arguments ty_lfts {_ _} _ {_}.
 Arguments ty_wf_E {_ _} _ {_}.
 
 Definition ty_outlives_E `{typeG Σ} ty `{!TyWf ty} (κ : lft) : elctx :=
-  (λ α, κ ⊑ α)%EL <$> ty.(ty_lfts).
+  (λ α, κ ⊑ₑ α) <$> ty.(ty_lfts).
 
 Lemma ty_outlives_E_elctx_sat `{typeG Σ} E L ty `{!TyWf ty} α β :
   ty.(ty_outlives_E) β ⊆+ E →
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index e31f4870..7b1b47e9 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -14,18 +14,9 @@ Inductive tctx_elt `{typeG Σ} : Type :=
 
 Notation tctx := (list tctx_elt).
 
-Delimit Scope lrust_tctx_scope with TC.
-Bind Scope lrust_tctx_scope with tctx_elt.
-
-Notation "p ◁ ty" := (TCtx_hasty p ty%list%T) (at level 70) : lrust_tctx_scope.
+Notation "p ◁ ty" := (TCtx_hasty p ty%list%T) (at level 70).
 Notation "p ◁{ κ } ty" := (TCtx_blocked p κ ty)
-   (at level 70, format "p  ◁{ κ }  ty") : lrust_tctx_scope.
-Notation "a :: b" := (@cons tctx_elt a%TC b%TC)
-  (at level 60, right associativity) : lrust_tctx_scope.
-Notation "[ x1 ; x2 ; .. ; xn ]" :=
-  (@cons tctx_elt x1%TC (@cons tctx_elt x2%TC
-        (..(@cons tctx_elt xn%TC (@nil tctx_elt))..))) : lrust_tctx_scope.
-Notation "[ x ]" := (@cons tctx_elt x%TC (@nil tctx_elt)) : lrust_tctx_scope.
+   (at level 70, format "p  ◁{ κ }  ty").
 
 Section type_context.
   Context `{typeG Σ}.
@@ -74,8 +65,8 @@ Section type_context.
   (** Type context element *)
   Definition tctx_elt_interp (tid : thread_id) (x : tctx_elt) : iProp Σ :=
     match x with
-    | (p ◁ ty)%TC => ∃ v, ⌜eval_path p = Some v⌝ ∗ ty.(ty_own) tid [v]
-    | (p ◁{κ} ty)%TC => ∃ v, ⌜eval_path p = Some v⌝ ∗
+    | p ◁ ty => ∃ v, ⌜eval_path p = Some v⌝ ∗ ty.(ty_own) tid [v]
+    | p ◁{κ} ty => ∃ v, ⌜eval_path p = Some v⌝ ∗
                              ([†κ] ={⊤}=∗ ty.(ty_own) tid [v])
     end%I.
 
@@ -122,7 +113,6 @@ Section type_context.
   (** Type context *)
   Definition tctx_interp (tid : thread_id) (T : tctx) : iProp Σ :=
     ([∗ list] x ∈ T, tctx_elt_interp tid x)%I.
-  Global Arguments tctx_interp _ _%TC.
 
   Global Instance tctx_interp_permut tid:
     Proper ((≡ₚ) ==> (⊣⊢)) (tctx_interp tid).
@@ -146,7 +136,6 @@ Section type_context.
   (** Copy typing contexts *)
   Class CopyC (T : tctx) :=
     copyc_persistent tid : PersistentP (tctx_interp tid T).
-  Global Arguments CopyC _%TC.
   Global Existing Instances copyc_persistent.
 
   Global Instance tctx_nil_copy : CopyC [].
@@ -159,7 +148,6 @@ Section type_context.
   (** Send typing contexts *)
   Class SendC (T : tctx) :=
     sendc_change_tid tid1 tid2 : tctx_interp tid1 T -∗ tctx_interp tid2 T.
-  Global Arguments SendC _%TC.
 
   Global Instance tctx_nil_send : SendC [].
   Proof. done. Qed.
@@ -178,7 +166,6 @@ Section type_context.
   Definition tctx_incl (E : elctx) (L : llctx) (T1 T2 : tctx): Prop :=
     ∀ tid q2, lft_ctx -∗ elctx_interp E -∗ llctx_interp L q2 -∗
               tctx_interp tid T1 ={⊤}=∗ llctx_interp L q2 ∗ tctx_interp tid T2.
-  Global Arguments tctx_incl _%EL _%LL _%TC _%TC.
   Global Instance : ∀ E L, RewriteRelation (tctx_incl E L).
 
   Global Instance tctx_incl_preorder E L : PreOrder (tctx_incl E L).
@@ -219,9 +206,9 @@ Section type_context.
   Proof. iIntros (??) "_ _ $ * [#$ $] //". Qed.
 
   Lemma copy_elem_of_tctx_incl E L T p `{!Copy ty} :
-    (p ◁ ty)%TC ∈ T → tctx_incl E L T ((p ◁ ty) :: T).
+    p ◁ ty ∈ T → tctx_incl E L T ((p ◁ ty) :: T).
   Proof.
-    remember (p ◁ ty)%TC. induction 1 as [|???? IH]; subst.
+    remember (p ◁ ty). induction 1 as [|???? IH]; subst.
     - apply (tctx_incl_frame_r _ [_] [_;_]), copy_tctx_incl, _.
     - etrans. by apply (tctx_incl_frame_l [_]), IH, reflexivity.
       apply contains_tctx_incl, submseteq_swap.
@@ -239,7 +226,6 @@ Section type_context.
 
   Definition tctx_extract_hasty E L p ty T T' : Prop :=
     tctx_incl E L T ((p ◁ ty)::T').
-  Global Arguments tctx_extract_hasty _%EL _%LL _%E _%T _%TC _%TC.
   Lemma tctx_extract_hasty_further E L p ty T T' x :
     tctx_extract_hasty E L p ty T T' →
     tctx_extract_hasty E L p ty (x::T) (x::T').
@@ -263,7 +249,6 @@ Section type_context.
 
   Definition tctx_extract_blocked E L p κ ty T T' : Prop :=
     tctx_incl E L T ((p ◁{κ} ty)::T').
-  Global Arguments tctx_extract_blocked _%EL _%LL _%E _ _%T _%TC _%TC.
   Lemma tctx_extract_blocked_cons E L p κ ty T T' x :
     tctx_extract_blocked E L p κ ty T T' →
     tctx_extract_blocked E L p κ ty (x::T) (x::T').
@@ -277,7 +262,6 @@ Section type_context.
 
   Definition tctx_extract_ctx E L T T1 T2 : Prop :=
     tctx_incl E L T1 (T++T2).
-  Global Arguments tctx_extract_ctx _%EL _%LL _%TC _%TC _%TC.
   Lemma tctx_extract_ctx_nil E L T:
     tctx_extract_ctx E L [] T T.
   Proof. by unfold tctx_extract_ctx. Qed.
@@ -306,7 +290,6 @@ Section type_context.
 
   Class UnblockTctx (κ : lft) (T1 T2 : tctx) : Prop :=
     unblock_tctx : ∀ tid, [†κ] -∗ tctx_interp tid T1 ={⊤}=∗ tctx_interp tid T2.
-  Global Arguments UnblockTctx _ _%TC _%TC.
 
   Global Instance unblock_tctx_nil κ : UnblockTctx κ [] [].
   Proof. by iIntros (tid) "_ $". Qed.
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index 93dbce64..33dbb662 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -132,7 +132,7 @@ Section case.
   Qed.
 
   Lemma type_case_shr E L C T p κ tyl el :
-    (p ◁ &shr{κ}sum tyl)%TC ∈ 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).
@@ -144,7 +144,7 @@ Section case.
   Lemma type_sum_assign_instr {E L} (i : nat) ty1 tyl ty ty2 p1 p2 :
     tyl !! i = Some ty →
     typed_write E L ty1 (sum tyl) ty2 →
-    typed_instruction E L [p1 ◁ ty1; p2 ◁ ty] (p1 <-{Σ i} p2) (λ _, [p1 ◁ ty2]%TC).
+    typed_instruction E L [p1 ◁ ty1; p2 ◁ ty] (p1 <-{Σ i} p2) (λ _, [p1 ◁ ty2]).
   Proof.
     iIntros (Hty Hw tid) "#LFT #HE $ HL Hp".
     rewrite tctx_interp_cons tctx_interp_singleton.
@@ -184,7 +184,7 @@ Section case.
   Lemma type_sum_unit_instr {E L} (i : nat) tyl ty1 ty2 p :
     tyl !! i = Some unit →
     typed_write E L ty1 (sum tyl) ty2 →
-    typed_instruction E L [p ◁ ty1] (p <-{Σ i} ()) (λ _, [p ◁ ty2]%TC).
+    typed_instruction E L [p ◁ ty1] (p <-{Σ i} ()) (λ _, [p ◁ ty2]).
   Proof.
     iIntros (Hty Hw tid) "#LFT #HE $ HL Hp". rewrite tctx_interp_singleton.
     wp_bind p. iApply (wp_hasty with "Hp"). iIntros (v Hv) "Hty".
@@ -215,7 +215,7 @@ Section case.
     typed_write E L ty1 (sum tyl) ty1' →
     typed_read E L ty2 ty ty2' →
     typed_instruction E L [p1 ◁ ty1; p2 ◁ ty2]
-               (p1 <-{ty.(ty_size),Σ i} !p2) (λ _, [p1 ◁ ty1'; p2 ◁ ty2']%TC).
+               (p1 <-{ty.(ty_size),Σ i} !p2) (λ _, [p1 ◁ ty1'; p2 ◁ ty2']).
   Proof.
     iIntros (Hty Hw Hr tid) "#LFT #HE Htl [HL1 HL2] Hp".
     rewrite tctx_interp_cons tctx_interp_singleton.
-- 
GitLab