diff --git a/theories/typing/fixpoint.v b/theories/typing/fixpoint.v
index b35258a6e53b1dac02b8e9b0c030a1d536a71b9c..01ffd0e53431473e214daa1121cccf7920d07bea 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 9eed7c5ece088bc0335118e3a058505ee90da650..cba36f427686f98a6106e68a6aaaa86aa7f24bf9 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -11,7 +11,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 0cf17a54ecf73839606c40a4a629e6237610e207..b1dcc9766a3aba7da10f248dee52fc2a7ef8c6c2 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -161,7 +161,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.
@@ -274,7 +274,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.
@@ -837,7 +837,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 9645ecbd03242b0d964497cf481cf8f6e99c7340..104a1a2c750c8e231a77d40bfbca1a120f6482a0 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/ghostcell.v b/theories/typing/lib/ghostcell.v
index 7085874bde001bff6df59ec16ce72c62070ec8c3..b66130a00108ce592ae3b437d94da2b3958e93ae 100644
--- a/theories/typing/lib/ghostcell.v
+++ b/theories/typing/lib/ghostcell.v
@@ -321,7 +321,7 @@ Section ghostcell.
   Qed.
 
   Global Instance ghostcell_wf α `{!TyWf ty} : TyWf (ghostcell α 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 ghostcell_type_ne α : TypeNonExpansive (ghostcell α).
   Proof.
diff --git a/theories/typing/lib/mutex/mutex.v b/theories/typing/lib/mutex/mutex.v
index ca3cd06d6e12082bbea321f95ad3c31aa5f6ab5c..65bbe7f92f4bc873ffaae0a09f935537d1a4fb6c 100644
--- a/theories/typing/lib/mutex/mutex.v
+++ b/theories/typing/lib/mutex/mutex.v
@@ -73,7 +73,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 960c7464935f3b863c125fb94b03ffce6b6f91f6..6ee38f834c3be478d41ea43c90a4ba370379e753 100644
--- a/theories/typing/lib/mutex/mutexguard.v
+++ b/theories/typing/lib/mutex/mutexguard.v
@@ -73,7 +73,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 2f7258297352c295b1602c694df55ea3b5d778d8..10c15e9128c9c592778940511fe2787902d59d6c 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -194,7 +194,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.
@@ -652,7 +652,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 a218e1de61bbc9203de3c16b75ecfa4945641c99..b9ad6cd0638e7aa2d41eb41e604526cc5c602c9c 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -65,7 +65,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 7ee34cc9fc753e340fb973b040318148c89f6c8c..cd37e6b84291e9680b98d8ff0bed2e5f6bbb4d64 100644
--- a/theories/typing/lib/refcell/ref.v
+++ b/theories/typing/lib/refcell/ref.v
@@ -70,7 +70,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 15ffbb559ab335ed417e8c11b61a8b34c5d67e97..7ccd3888213a9c35bc269cf1f5d124f0187e38b9 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -165,7 +165,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 b405995b96879acac27d3134e72df0640337713a..2549cc0decd535288c6ea0a41e506d453be076ed 100644
--- a/theories/typing/lib/refcell/refmut.v
+++ b/theories/typing/lib/refcell/refmut.v
@@ -75,7 +75,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 ad9ef92c312820867baa75a6c9d0c4f4b0f8f176..7713024853a3774d725dcd8570be6ea95777b1bd 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -172,7 +172,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 51df1e84e91298de8dd1e0fdf60bda6cd2fb83f0..d4741c2116a0cc5481ecd63eb93658208a5f114f 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 702201bc7561fd202e987376fb7a47430c1d2f0e..620afee43f7af93afba229850cb4333fd8c88514 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard.v
@@ -63,7 +63,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 421bb191bd4dba82038f5e57749a439bb1bd957c..6fc0af6baa6ba1282f85b2cdeac05c93d0d8e98f 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 757e883c726a2e82fdf0dd81018ab2891fe67f08..c0db77cfa772407b297da3c8a63468d50cbd99c6 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -87,7 +87,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 0fb7bf7fbbff4630d74f866a0d9e95d9d5d4c79b..360c9672b2890f34c61a62131a22eda9cc0e1061 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 ea9fa41395074bbca4ac58566f9c39cf776a0b2b..33339544c15b4df6563ed163844af1957d1e904b 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -57,14 +57,14 @@ Arguments ty_lfts {_ _} _ {_}.
 Arguments ty_wf_E {_ _} _ {_}.
 
 Definition ty_outlives_E `{!typeGS Σ} ty `{!TyWf ty} (κ : lft) : elctx :=
-  (λ α, κ ⊑ₑ α) <$> ty.(ty_lfts).
+  (λ α, κ ⊑ₑ α) <$> (ty_lfts ty).
 
 Lemma ty_outlives_E_elctx_sat `{!typeGS Σ} 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.
@@ -82,15 +82,15 @@ Existing Instances list_ty_wf_nil list_ty_wf_cons.
 Fixpoint tyl_lfts `{!typeGS Σ} 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 `{!typeGS Σ} 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 `{!typeGS Σ} tyl {WF : ListTyWf tyl} (κ : lft) : elctx :=
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index 3813dd687668b0c23568eb33462f9f854eede474..742c8c95be15520ebb6fd59c6be86f7335d855c0 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -42,7 +42,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 -∗