diff --git a/theories/typing/fixpoint.v b/theories/typing/fixpoint.v
index dc64f4ae91a499cc682e52b0c69f5f235a010274..fa8f989e1849bb2c653c1c7c80a7614194a431ea 100644
--- a/theories/typing/fixpoint.v
+++ b/theories/typing/fixpoint.v
@@ -28,11 +28,11 @@ Section fixpoint_def.
   Global Instance type_fixpoint_wf `{!∀ `{!TyWf ty}, TyWf (T ty)} : TyWf type_fixpoint :=
     let lfts :=
       let _ : TyWf type_fixpoint := {| ty_lfts := []; ty_wf_E := [] |} in
-      (T type_fixpoint).(ty_lfts)
+      ty_lfts (T type_fixpoint)
     in
     let wf_E :=
       let _ : TyWf type_fixpoint := {| ty_lfts := lfts; ty_wf_E := [] |} in
-      (T type_fixpoint).(ty_wf_E)
+      ty_wf_E (T type_fixpoint)
     in
     {| ty_lfts := lfts; ty_wf_E := wf_E |}.
 End fixpoint_def.
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 3faa1a71b9a9594719ec88e4ea6f5a6e3b3a1521..246d4334eef34bb62909b11b1679659df097d4bb 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -12,7 +12,7 @@ Section fn.
 
   Definition FP_wf E (tys : vec type n) `{!ListTyWf tys} ty `{!TyWf ty} :=
     FP (λ ϝ, E ϝ ++ tyl_wf_E tys ++ tyl_outlives_E tys ϝ ++
-                    ty.(ty_wf_E) ++ ty_outlives_E ty ϝ)
+                    ty_wf_E ty ++ ty_outlives_E ty ϝ)
        tys ty.
 
   (* The other alternative for defining the fn type would be to state
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index f584e7c562f6925c8f09dc6fceeed68c3e42e4b8..e976a095de860622c8e6f6ce03f34cf44a6cdb80 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -221,7 +221,7 @@ Section arc.
   Qed.
 
   Global Instance arc_wf ty `{!TyWf ty} : TyWf (arc ty) :=
-    { ty_lfts := ty.(ty_lfts); ty_wf_E := ty.(ty_wf_E) }.
+    { ty_lfts := ty_lfts ty; ty_wf_E := ty_wf_E ty }.
 
   Global Instance arc_type_contractive : TypeContractive arc.
   Proof.
@@ -346,7 +346,7 @@ Section arc.
   Qed.
 
   Global Instance weak_wf ty `{!TyWf ty} : TyWf (weak ty) :=
-    { ty_lfts := ty.(ty_lfts); ty_wf_E := ty.(ty_wf_E) }.
+    { ty_lfts := ty_lfts ty; ty_wf_E := ty_wf_E ty }.
 
   Global Instance weak_type_contractive : TypeContractive weak.
   Proof.
@@ -941,7 +941,7 @@ Section arc.
   (* Code : other primitives *)
   Definition arc_try_unwrap ty : val :=
     fn: ["arc"] :=
-      let: "r" := new [ #(Σ[ ty; arc ty ]).(ty_size) ] in
+      let: "r" := new [ #(ty_size Σ[ ty; arc ty ]) ] in
       let: "arc'" := !"arc" in
       if: try_unwrap ["arc'"] then
         (* Return content *)
diff --git a/theories/typing/lib/cell.v b/theories/typing/lib/cell.v
index 9754ad218ae0a349abd78fc1084ee32d1e4919dd..514fbd75ad2c85b25d45055c2129ed9d6b69af20 100644
--- a/theories/typing/lib/cell.v
+++ b/theories/typing/lib/cell.v
@@ -21,7 +21,7 @@ Section cell.
   Qed.
 
   Global Instance cell_wf ty `{!TyWf ty} : TyWf (cell ty) :=
-    { ty_lfts := ty.(ty_lfts); ty_wf_E := ty.(ty_wf_E) }.
+    { ty_lfts := ty_lfts ty; ty_wf_E := ty_wf_E ty }.
 
   Global Instance cell_type_ne : TypeNonExpansive cell.
   Proof. solve_type_proper. Qed.
diff --git a/theories/typing/lib/mutex/mutex.v b/theories/typing/lib/mutex/mutex.v
index 6452d0de2bf18d8da4472da7bd8ff09b07b8383f..6d4f19975e42c318af099d1002df85d936e44f49 100644
--- a/theories/typing/lib/mutex/mutex.v
+++ b/theories/typing/lib/mutex/mutex.v
@@ -67,7 +67,7 @@ Section mutex.
   Qed.
 
   Global Instance mutex_wf ty `{!TyWf ty} : TyWf (mutex ty) :=
-    { ty_lfts := ty.(ty_lfts); ty_wf_E := ty.(ty_wf_E) }.
+    { ty_lfts := ty_lfts ty; ty_wf_E := ty_wf_E ty }.
 
   Global Instance mutex_type_ne : TypeNonExpansive mutex.
   Proof.
diff --git a/theories/typing/lib/mutex/mutexguard.v b/theories/typing/lib/mutex/mutexguard.v
index 471c21e6eaa45ef07dfb3b01ec9d7dd89d197f72..6cb50d7220a96dfb749c56430c8d387966043475 100644
--- a/theories/typing/lib/mutex/mutexguard.v
+++ b/theories/typing/lib/mutex/mutexguard.v
@@ -72,7 +72,7 @@ Section mguard.
   Qed.
 
   Global Instance mutexguard_wf α ty `{!TyWf ty} : TyWf (mutexguard α ty) :=
-    { ty_lfts := [α]; ty_wf_E := ty.(ty_wf_E) ++ ty_outlives_E ty α }.
+    { ty_lfts := [α]; ty_wf_E := ty_wf_E ty ++ ty_outlives_E ty α }.
 
   Global Instance mutexguard_type_contractive α : TypeContractive (mutexguard α).
   Proof.
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index d3c5b1944760a3afdab496b5df74a22f4a6908a0..193629bbdea230290561a9c4b33d2e9b941a47f3 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -201,7 +201,7 @@ Section rc.
   Qed.
 
   Global Instance rc_wf ty `{!TyWf ty} : TyWf (rc ty) :=
-    { ty_lfts := ty.(ty_lfts); ty_wf_E := ty.(ty_wf_E) }.
+    { ty_lfts := ty_lfts ty; ty_wf_E := ty_wf_E ty }.
 
   Global Instance rc_type_contractive : TypeContractive rc.
   Proof.
@@ -659,7 +659,7 @@ Section code.
 
   Definition rc_try_unwrap ty : val :=
     fn: ["rc"] :=
-      let: "r" := new [ #(Σ[ ty; rc ty ]).(ty_size) ] in
+      let: "r" := new [ #(ty_size Σ[ ty; rc ty ]) ] in
     withcont: "k":
       let: "rc'" := !"rc" in
       let: "strong" := !("rc'" +â‚— #0) in
diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v
index 6df9fa6724bed909f19144800490416c22b094da..b6c6befbd6f010c078b98fb7af556af8931dea74 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -71,7 +71,7 @@ Section weak.
   Qed.
 
   Global Instance weak_wf ty `{!TyWf ty} : TyWf (weak ty) :=
-    { ty_lfts := ty.(ty_lfts); ty_wf_E := ty.(ty_wf_E) }.
+    { ty_lfts := ty_lfts ty; ty_wf_E := ty_wf_E ty }.
 
   Global Instance weak_type_contractive : TypeContractive weak.
   Proof.
diff --git a/theories/typing/lib/refcell/ref.v b/theories/typing/lib/refcell/ref.v
index 8c3e2f0cab611084fa127d787269fc6d0632d358..7de2d42616e85a042c8a33b35f6f86ed299f271e 100644
--- a/theories/typing/lib/refcell/ref.v
+++ b/theories/typing/lib/refcell/ref.v
@@ -69,7 +69,7 @@ Section ref.
   Qed.
 
   Global Instance ref_wf α ty `{!TyWf ty} : TyWf (ref α ty) :=
-    { ty_lfts := [α]; ty_wf_E := ty.(ty_wf_E) ++ ty_outlives_E ty α }.
+    { ty_lfts := [α]; ty_wf_E := ty_wf_E ty ++ ty_outlives_E ty α }.
 
   Global Instance ref_type_contractive α : TypeContractive (ref α).
   Proof. solve_type_proper. Qed.
diff --git a/theories/typing/lib/refcell/refcell.v b/theories/typing/lib/refcell/refcell.v
index 6d60ef565534de864f9fd3799bc7eb4482c89b6d..413bb764ac3700828f83f3582de15bf1e1e133f8 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -164,7 +164,7 @@ Section refcell.
   Qed.
 
   Global Instance refcell_wf ty `{!TyWf ty} : TyWf (refcell ty) :=
-    { ty_lfts := ty.(ty_lfts); ty_wf_E := ty.(ty_wf_E) }.
+    { ty_lfts := ty_lfts ty; ty_wf_E := ty_wf_E ty }.
 
   Global Instance refcell_type_ne : TypeNonExpansive refcell.
   Proof.
diff --git a/theories/typing/lib/refcell/refmut.v b/theories/typing/lib/refcell/refmut.v
index 65cd958d91e938193286e78cf7f5c3bf3d1d990c..57402d42bb78ec8070e10f630ec0280827a4a323 100644
--- a/theories/typing/lib/refcell/refmut.v
+++ b/theories/typing/lib/refcell/refmut.v
@@ -74,7 +74,7 @@ Section refmut.
   Qed.
 
   Global Instance refmut_wf α ty `{!TyWf ty} : TyWf (refmut α ty) :=
-    { ty_lfts := [α]; ty_wf_E := ty.(ty_wf_E) ++ ty_outlives_E ty α }.
+    { ty_lfts := [α]; ty_wf_E := ty_wf_E ty ++ ty_outlives_E ty α }.
 
   Global Instance refmut_type_contractive α : TypeContractive (refmut α).
   Proof. solve_type_proper. Qed.
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index 5c4f50cd5a3e6121c75f39d8be9126e111802704..f1e71df7614e22d29f0f3a8da9aa9628741fc8dc 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -415,7 +415,7 @@ Section rwlock.
   Qed.
 
   Global Instance rwlock_wf ty `{!TyWf ty} : TyWf (rwlock ty) :=
-    { ty_lfts := ty.(ty_lfts); ty_wf_E := ty.(ty_wf_E) }.
+    { ty_lfts := ty_lfts ty; ty_wf_E := ty_wf_E ty }.
 
   Global Instance rwlock_type_ne : TypeNonExpansive rwlock.
   Proof.
diff --git a/theories/typing/lib/rwlock/rwlockreadguard.v b/theories/typing/lib/rwlock/rwlockreadguard.v
index 8e2910431db1fa6877fdb805e120a793442ea8ca..af08b2af9c2acdf0b7d2dd43202d4a77f1600cdc 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard.v
@@ -63,7 +63,7 @@ Section rwlockreadguard.
   Qed.
 
   Global Instance rwlockreadguard_wf α ty `{!TyWf ty} : TyWf (rwlockreadguard α ty) :=
-    { ty_lfts := [α]; ty_wf_E := ty.(ty_wf_E) ++ ty_outlives_E ty α }.
+    { ty_lfts := [α]; ty_wf_E := ty_wf_E ty ++ ty_outlives_E ty α }.
 
   Global Instance rwlockreadguard_type_contractive α : TypeContractive (rwlockreadguard α).
   Proof.
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard.v b/theories/typing/lib/rwlock/rwlockwriteguard.v
index 77b1f4385242342f7bea37f712bbda7a91e1ca96..368a7b603bb9c5cec9735fc077afe3a5b6169f19 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard.v
@@ -65,7 +65,7 @@ Section rwlockwriteguard.
   Qed.
 
   Global Instance rwlockwriteguard_wf α ty `{!TyWf ty} : TyWf (rwlockwriteguard α ty) :=
-    { ty_lfts := [α]; ty_wf_E := ty.(ty_wf_E) ++ ty_outlives_E ty α }.
+    { ty_lfts := [α]; ty_wf_E := ty_wf_E ty ++ ty_outlives_E ty α }.
 
   Global Instance rwlockwriteguard_type_contractive α : TypeContractive (rwlockwriteguard α).
   Proof.
diff --git a/theories/typing/lib/spawn.v b/theories/typing/lib/spawn.v
index eb57e95fa0468f99e3f34b3b0dfedc117fdec271..c88073a91ed0f9d73abcdac12fdf77073ad96754 100644
--- a/theories/typing/lib/spawn.v
+++ b/theories/typing/lib/spawn.v
@@ -25,7 +25,7 @@ Section join_handle.
   Next Obligation. iIntros (?) "**"; auto. Qed.
 
   Global Instance join_handle_wf ty `{!TyWf ty} : TyWf (join_handle ty) :=
-    { ty_lfts := ty.(ty_lfts); ty_wf_E := ty.(ty_wf_E) }.
+    { ty_lfts := ty_lfts ty; ty_wf_E := ty_wf_E ty }.
 
   Lemma join_handle_subtype ty1 ty2 :
     ▷ type_incl ty1 ty2 -∗ type_incl (join_handle ty1) (join_handle ty2).
diff --git a/theories/typing/own.v b/theories/typing/own.v
index f14a983cad86e5f073e097777be0682c7a7eb257..27dbbb06c0a44414fdce8707409116779d3808d8 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -88,7 +88,7 @@ Section own.
   Qed.
 
   Global Instance own_ptr_wf n ty `{!TyWf ty} : TyWf (own_ptr n ty) :=
-    { ty_lfts := ty.(ty_lfts); ty_wf_E := ty.(ty_wf_E) }.
+    { ty_lfts := ty_lfts ty; ty_wf_E := ty_wf_E ty }.
 
   Lemma own_type_incl n m ty1 ty2 :
     ▷ ⌜n = m⌝ -∗ ▷ type_incl ty1 ty2 -∗ type_incl (own_ptr n ty1) (own_ptr m ty2).
diff --git a/theories/typing/shr_bor.v b/theories/typing/shr_bor.v
index e6042d95081afc2f6a9713cb8924718d801f90f2..1b723d933e571bb3ec13be9d4918b4682d88b146 100644
--- a/theories/typing/shr_bor.v
+++ b/theories/typing/shr_bor.v
@@ -16,7 +16,7 @@ Section shr_bor.
   Next Obligation. intros κ ty tid [|[[]|][]]; apply _. Qed.
 
   Global Instance shr_bor_wf κ ty `{!TyWf ty} : TyWf (shr_bor κ ty) :=
-    { ty_lfts := [κ]; ty_wf_E := ty.(ty_wf_E) ++ ty_outlives_E ty κ }.
+    { ty_lfts := [κ]; ty_wf_E := ty_wf_E ty ++ ty_outlives_E ty κ }.
 
   Lemma shr_type_incl κ1 κ2 ty1 ty2 :
     κ2 ⊑ κ1 -∗ type_incl ty1 ty2 -∗ type_incl (shr_bor κ1 ty1) (shr_bor κ2 ty2).
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 183eb2d280b55a50bd721909ff34b2b57b59a60f..f1d22fad901f74830476ab77d4b7fe9cd47ef1b8 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -62,14 +62,14 @@ Arguments ty_lfts {_ _} _ {_}.
 Arguments ty_wf_E {_ _} _ {_}.
 
 Definition ty_outlives_E `{!typeG Σ} ty `{!TyWf ty} (κ : lft) : elctx :=
-  (λ α, κ ⊑ₑ α) <$> ty.(ty_lfts).
+  (λ α, κ ⊑ₑ α) <$> (ty_lfts ty).
 
 Lemma ty_outlives_E_elctx_sat `{!typeG Σ} E L ty `{!TyWf ty} α β :
   ty_outlives_E ty β ⊆+ E →
   lctx_lft_incl E L α β →
   elctx_sat E L (ty_outlives_E ty α).
 Proof.
-  unfold ty_outlives_E. induction ty.(ty_lfts) as [|κ l IH]=>/= Hsub Hαβ.
+  unfold ty_outlives_E. induction (ty_lfts ty) as [|κ l IH]=>/= Hsub Hαβ.
   - solve_typing.
   - apply elctx_sat_lft_incl.
     + etrans; first done. eapply lctx_lft_incl_external, elem_of_submseteq, Hsub.
@@ -87,15 +87,15 @@ Existing Instances list_ty_wf_nil list_ty_wf_cons.
 Fixpoint tyl_lfts `{!typeG Σ} tyl {WF : ListTyWf tyl} : list lft :=
   match WF with
   | list_ty_wf_nil => []
-  | list_ty_wf_cons ty [] => ty.(ty_lfts)
-  | list_ty_wf_cons ty tyl => ty.(ty_lfts) ++ tyl.(tyl_lfts)
+  | list_ty_wf_cons ty [] => ty_lfts ty
+  | list_ty_wf_cons ty tyl => ty_lfts ty ++ tyl_lfts tyl
   end.
 
 Fixpoint tyl_wf_E `{!typeG Σ} tyl {WF : ListTyWf tyl} : elctx :=
   match WF with
   | list_ty_wf_nil => []
-  | list_ty_wf_cons ty [] => ty.(ty_wf_E)
-  | list_ty_wf_cons ty tyl => ty.(ty_wf_E) ++ tyl.(tyl_wf_E)
+  | list_ty_wf_cons ty [] => ty_wf_E ty
+  | list_ty_wf_cons ty tyl => ty_wf_E ty ++ tyl_wf_E tyl
   end.
 
 Fixpoint tyl_outlives_E `{!typeG Σ} tyl {WF : ListTyWf tyl} (κ : lft) : elctx :=
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index 4747f0f7816466a0f78190296dbecd1936663f7e..40f68513971f9d3611e89975410d03f12514b14f 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -41,7 +41,7 @@ Section uniq_bor.
   Qed.
 
   Global Instance uniq_bor_wf κ ty `{!TyWf ty} : TyWf (uniq_bor κ ty) :=
-    { ty_lfts := [κ]; ty_wf_E := ty.(ty_wf_E) ++ ty_outlives_E ty κ }.
+    { ty_lfts := [κ]; ty_wf_E := ty_wf_E ty ++ ty_outlives_E ty κ }.
 
   Lemma uniq_type_incl κ1 κ2 ty1 ty2 :
     κ2 ⊑ κ1 -∗