diff --git a/theories/lifetime/model/accessors.v b/theories/lifetime/model/accessors.v
index 82af0c04f6280595d4543fa6609bf3c699e529fe..084510de1553f9f94a5d69b318df7f2603e4fdec 100644
--- a/theories/lifetime/model/accessors.v
+++ b/theories/lifetime/model/accessors.v
@@ -390,7 +390,7 @@ Proof.
     iSpecialize ("HQ" with "[//]"). rewrite -monPred_at_later.
     iApply "HPP'V". iApply ("HvsQ" with "HQ H†"). }
   iExists _, _. iFrame. rewrite big_sepS_later. iApply "Hclose''".
-  iExists _. iFrame "%". iLeft. rewrite lft_inv_alive_unfold. iExists _, _. iFrame. 
+  iExists _. iFrame "%". iLeft. rewrite lft_inv_alive_unfold. iExists _, _. iFrame.
   iNext. rewrite -!fmap_delete -fmap_insert -(fmap_insert _ _ _ (Bor_in Vb)).
   rewrite /lft_bor_alive. iExists _. iFrame "Hbox H●".
   rewrite big_sepM_insert. by rewrite big_sepM_delete.
diff --git a/theories/lifetime/model/borrow_sep.v b/theories/lifetime/model/borrow_sep.v
index 324d330cc0e924356ed971f737f74ec376a70b7c..7ce4049021d6cad1cbfa67053d389c1c08504f86 100644
--- a/theories/lifetime/model/borrow_sep.v
+++ b/theories/lifetime/model/borrow_sep.v
@@ -126,9 +126,9 @@ Proof.
   iIntros (?) "#LFT HP HQ". rewrite {1 2}/bor.
   iDestruct "HP" as (κ1) "[#Hκ1 Hbor1]". iDestruct "HQ" as (κ2) "[#Hκ2 Hbor2]".
   iMod (raw_bor_shorten _ _ (κ1 ⊓ κ2) with "LFT Hbor1") as "Hbor1".
-    done. by apply gmultiset_union_subseteq_l.
+    done. by apply gmultiset_disj_union_subseteq_l.
   iMod (raw_bor_shorten _ _ (κ1 ⊓ κ2) with "LFT Hbor2") as "Hbor2".
-    done. by apply gmultiset_union_subseteq_r.
+    done. by apply gmultiset_disj_union_subseteq_r.
   iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose". unfold raw_bor, idx_bor_own.
   iDestruct "Hbor1" as (j1) "[Hbor1 Hslice1]". iDestruct "Hbor2" as (j2) "[Hbor2 Hslice2]".
   iDestruct "Hbor1" as (V1) "[#HV1 Hbor1]". iDestruct "Hbor2" as (V2) "[#HV2 Hbor2]".
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index 75bda3aeb08c8cc21151beff4003df18cf474b83..ef40902194e7e740f8838ce82b757fc4d188e59a 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -65,7 +65,7 @@ Lemma lfts_kill A (I : gmap lft lft_names) (K K' : gset lft) (Vs : lft → Lat)
     ={↑borN ∪ ↑inhN ∪ E0}=∗ Iinv K' ∗ [∗ set] κ ∈ K, lft_inv_dead κ (Vs κ).
 Proof.
   intros Iinv HVs. revert K'.
-  induction (collection_wf K) as [K _ IH]=> K' HKK' HKK'I HK.
+  induction (set_wf K) as [K _ IH]=> K' HKK' HKK'I HK.
   iIntros "[HI Halive] HK".
   pose (Kalive := filter (lft_alive_in A) K).
   destruct (decide (Kalive = ∅)) as [HKalive|].
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index 4d8a6de81d4f21267ae9e7bfcf8641525be6e9e9..1b1c2de8e04cc7ddd17a8e7c4e1442d977df8b6f 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -19,7 +19,7 @@ Module Export lft_notation.
 End lft_notation.
 
 Definition static : lft := (∅ : gmultiset _).
-Instance lft_intersect : Meet lft := union.
+Instance lft_intersect : Meet lft := disj_union.
 
 Inductive bor_state {Lat} :=
   | Bor_in (V : Lat)
@@ -137,7 +137,7 @@ Section defs.
    Definition lft_inh (κ : lft) (s : option Lat) (Pi : monPred) : iProp :=
      (∃ E : gset slice_name,
        own_inh κ (● GSet E) ∗
-       box inhN (to_gmap s E) Pi)%I.
+       box inhN (gset_to_gmap s E) Pi)%I.
 
    Definition lft_vs_inv_go (κ : lft) (lft_inv_alive : ∀ κ', κ' ⊂ κ → Lat → iProp)
        (Vs : lft → Lat) (I : gmap lft lft_names) : iProp :=
diff --git a/theories/lifetime/model/faking.v b/theories/lifetime/model/faking.v
index d2798338f8e716cdcb6a19bb5dd96f33ab4b16dd..888bbd0254481b8d6d11d5ad070bb50a6309f03c 100644
--- a/theories/lifetime/model/faking.v
+++ b/theories/lifetime/model/faking.v
@@ -31,7 +31,7 @@ Proof.
   iAssert (own_cnt κ (◯ 0)) with "[Hcnt']" as "Hcnt'".
   { rewrite /own_cnt. iExists γs. by iFrame. }
   iAssert (∀ o, lft_inh κ o True)%I with "[Hinh]" as "Hinh".
-  { iIntros (o). rewrite /lft_inh. iExists ∅. rewrite to_gmap_empty.
+  { iIntros (o). rewrite /lft_inh. iExists ∅. rewrite gset_to_gmap_empty.
     iSplitL; [|iApply box_alloc]. rewrite /own_inh. iExists γs. by iFrame. }
   iAssert (lft_inv_dead κ bot ∧ lft_inv_alive κ bot)%I
     with "[-HA HI Hinv]" as "Hdeadandalive".
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index ba33ebbeaac3f0d3f3b9cbc07a6cd01993027315..66f0d929c6a938ead106571aa5baad1c7b33f8c4 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -228,7 +228,7 @@ Proof. exists Λ. by rewrite lookup_insert. Qed.
 Lemma lft_dead_in_alive_in_union κ κ' :
   lft_dead_in A (κ ⊓ κ') → lft_alive_in A κ → lft_dead_in A κ'.
 Proof.
-  intros (Λ & [Hin|Hin]%elem_of_union & HΛ) Halive.
+  intros (Λ & [Hin|Hin]%gmultiset_elem_of_disj_union & HΛ) Halive.
   - contradict HΛ. rewrite (Halive _ Hin). done.
   - exists Λ. auto.
 Qed.
@@ -274,7 +274,7 @@ Instance lft_intersect_left_id : LeftId eq static lft_intersect := _.
 Instance lft_intersect_right_id : RightId eq static lft_intersect := _.
 
 Lemma lft_tok_sep q κ1 κ2 : q.[κ1] ∗ q.[κ2] ⊣⊢ q.[κ1 ⊓ κ2].
-Proof. by rewrite /lft_tok -big_sepMS_union. Qed.
+Proof. by rewrite /lft_tok -big_sepMS_disj_union. Qed.
 
 Lemma lft_dead_or κ1 κ2 : [†κ1] ∨ [†κ2] ⊣⊢ [† κ1 ⊓ κ2].
 Proof.
@@ -447,10 +447,10 @@ Proof.
     as (γE) "(% & #Hslice & Hbox)".
   iMod (own_inh_update with "HE") as "[HE HE◯]".
   { by eapply auth_update_alloc, (gset_disj_alloc_empty_local_update _ {[γE]}),
-      disjoint_singleton_l, lookup_to_gmap_None. }
+      disjoint_singleton_l, lookup_gset_to_gmap_None. }
   iModIntro. iSplitL "Hbox HE".
   { iNext. rewrite /lft_inh. iExists ({[γE]} ∪ PE).
-    rewrite to_gmap_union_singleton. iFrame. }
+    rewrite gset_to_gmap_union_singleton. iFrame. }
   clear dependent PE. rewrite -(left_id_L ε op (◯ GSet {[γE]})).
   iDestruct "HE◯" as "[HE◯' HE◯]". iSplitL "HE◯'".
   { iIntros (I) "HI". iApply (own_inh_auth with "HI HE◯'"). }
@@ -461,11 +461,11 @@ Proof.
   { apply auth_update_dealloc, gset_disj_dealloc_local_update. }
   iMod (slice_delete_full _ _ true with "Hslice Hbox")
     as (Q'') "($ & #? & Hbox)"; first by solve_ndisj.
-  { rewrite lookup_to_gmap_Some. set_solver. }
+  { rewrite lookup_gset_to_gmap_Some. set_solver. }
   iModIntro. iExists Q''. iSplit; first done.
   iNext. rewrite /lft_inh. iExists (PE ∖ {[γE]}). iFrame "HE".
   rewrite {1}(union_difference_L {[ γE ]} PE); last set_solver.
-  rewrite to_gmap_union_singleton delete_insert // lookup_to_gmap_None.
+  rewrite gset_to_gmap_union_singleton delete_insert // lookup_gset_to_gmap_None.
   set_solver.
 Qed.
 
@@ -476,7 +476,7 @@ Proof.
   rewrite /lft_inh. iIntros (?) "[Hinh HQ]".
   iDestruct "Hinh" as (E') "[Hinh Hbox]".
   iMod (box_fill with "Hbox HQ") as "?"=>//.
-  rewrite fmap_to_gmap. iModIntro. iExists E'. by iFrame.
+  rewrite fmap_gset_to_gmap. iModIntro. iExists E'. by iFrame.
 Qed.
 
 (* View shifts *)
diff --git a/theories/lifetime/model/reborrow.v b/theories/lifetime/model/reborrow.v
index 8a643c7ec56b9cee7c1a1fccbe6f317f75f87be1..925ac0e678f68f92b171dc25beb4f3c44c088909 100644
--- a/theories/lifetime/model/reborrow.v
+++ b/theories/lifetime/model/reborrow.v
@@ -238,9 +238,9 @@ Proof.
   rewrite /idx_bor /bor. destruct i as [κ0 i].
   iDestruct "HP" as "[Hκκ0 HP]". iDestruct "HP" as (P') "[HPP' HP']".
   iMod (raw_bor_shorten _ _ (κ0 ⊓ κ'0) with "LFT Hbor") as "Hbor";
-    [done|by apply gmultiset_union_subseteq_r|].
+    [done|by apply gmultiset_disj_union_subseteq_r|].
   iMod (raw_idx_bor_unnest with "LFT HP' Hbor") as "Hbor";
-    [done|by apply gmultiset_union_subset_l|].
+    [done|by apply gmultiset_disj_union_subset_l|].
   iExists _. iDestruct (raw_bor_iff with "HPP' Hbor") as "$".
     by iApply lft_intersect_mono.
 Qed.
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 5f3cea938ddd9557a471528bf06226314772f881..b38097b850bb45b77a4aab3b20f4ee021f897db9 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -11,8 +11,8 @@ Section fn.
   Record fn_params := FP { fp_E : lft → elctx; fp_tys : vec type n; fp_ty : type }.
 
   Definition FP_wf E (tys : vec type n) `{!TyWfLst tys} ty `{!TyWf ty} :=
-    FP (λ ϝ, E ϝ ++ tys.(tyl_wf_E) ++ tys.(tyl_outlives_E) ϝ ++
-                    ty.(ty_wf_E) ++ ty.(ty_outlives_E) ϝ)
+    FP (λ ϝ, E ϝ ++ tyl_wf_E tys ++ tyl_outlives_E tys ϝ ++
+                    ty.(ty_wf_E) ++ ty_outlives_E ty ϝ)
        tys ty.
 
   (* The other alternative for defining the fn type would be to state
diff --git a/theories/typing/lib/diverging_static.v b/theories/typing/lib/diverging_static.v
index b07fdb62896f4c7cdb6ce9a28c33a5fe92d7e430..62fac42d7df3fe3035d9756f58b8c28870287fe6 100644
--- a/theories/typing/lib/diverging_static.v
+++ b/theories/typing/lib/diverging_static.v
@@ -22,7 +22,7 @@ Section diverging_static.
     (* F : FnOnce(&'static T), as witnessed by the impl call_once *)
     typed_val call_once (fn(∅; F, &shr{static} T) → unit) →
     typed_val (diverging_static_loop call_once)
-              (fn(∀ α, λ ϝ, T.(ty_outlives_E) static; &shr{α} T, F) → ∅).
+              (fn(∀ α, λ ϝ, ty_outlives_E T static; &shr{α} T, F) → ∅).
   Proof.
     intros Hf E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>x f. simpl_subst.
diff --git a/theories/typing/lib/mutex/mutexguard.v b/theories/typing/lib/mutex/mutexguard.v
index 091f67512a936e03e686b351c0f0ee03be96fe4d..0834d1ed0f0fba3bdab7af301675c50c39bc24cc 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.(ty_outlives_E) α }.
+    { ty_lfts := [α]; ty_wf_E := ty.(ty_wf_E) ++ ty_outlives_E ty α }.
 
   Global Instance mutexguard_type_contractive α : TypeContractive (mutexguard α).
   Proof.
diff --git a/theories/typing/lib/refcell/ref.v b/theories/typing/lib/refcell/ref.v
index 162511a45def79b1fb51ebfd35ea7b1fd90727fa..24fd5b888ae8142d0732af2ab14ff4d491a04886 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.(ty_outlives_E) α }.
+    { ty_lfts := [α]; ty_wf_E := ty.(ty_wf_E) ++ ty_outlives_E ty α }.
 
   Global Instance ref_type_contractive α : TypeContractive (ref α).
   Proof. solve_type_proper. Qed.
diff --git a/theories/typing/lib/refcell/refmut.v b/theories/typing/lib/refcell/refmut.v
index 6e2f94fb244a74039e7700636e1f7bb5f6cbab7e..ed13740bcbf9d538583bd04a9ad3ddc7e88d5641 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.(ty_outlives_E) α }.
+    { ty_lfts := [α]; ty_wf_E := ty.(ty_wf_E) ++ ty_outlives_E ty α }.
 
   Global Instance refmut_type_contractive α : TypeContractive (refmut α).
   Proof. solve_type_proper. Qed.
diff --git a/theories/typing/lib/rwlock/rwlockreadguard.v b/theories/typing/lib/rwlock/rwlockreadguard.v
index fda6590dcefe0501376ca4e441f3a9f44afafea9..1a6347111210771f6d1e676670c9b08db8f371f0 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard.v
@@ -62,7 +62,7 @@ Section rwlockreadguard.
   Qed.
 
   Global Instance rwlockreadguard_wf α ty `{!TyWf ty} : TyWf (rwlockreadguard α ty) :=
-    { ty_lfts := [α]; ty_wf_E := ty.(ty_wf_E) ++ ty.(ty_outlives_E) α }.
+    { ty_lfts := [α]; ty_wf_E := ty.(ty_wf_E) ++ 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 770c12fa0f795f5695fcde7dc51d163616b10de6..7d16364e5b99e62a59f1aa2801e9d1e3e2c5b4f9 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard.v
@@ -64,7 +64,7 @@ Section rwlockwriteguard.
   Qed.
 
   Global Instance rwlockwriteguard_wf α ty `{!TyWf ty} : TyWf (rwlockwriteguard α ty) :=
-    { ty_lfts := [α]; ty_wf_E := ty.(ty_wf_E) ++ ty.(ty_outlives_E) α }.
+    { ty_lfts := [α]; ty_wf_E := ty.(ty_wf_E) ++ 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 1c19d96054e31bc47b0a3a9d52c678e8805a7172..4ca1c03d6a1eec310ae7a201d84217a47cfc8da0 100644
--- a/theories/typing/lib/spawn.v
+++ b/theories/typing/lib/spawn.v
@@ -81,7 +81,7 @@ Section spawn.
   Lemma spawn_type fty retty call_once `{!TyWf fty, !TyWf retty}
         `(!Send fty, !Send retty) :
     typed_val call_once (fn(∅; fty) → retty) → (* fty : FnOnce() -> retty, as witnessed by the impl call_once *)
-    let E ϝ := fty.(ty_outlives_E) static ++ retty.(ty_outlives_E) static in
+    let E ϝ := ty_outlives_E fty static ++ ty_outlives_E retty static in
     typed_val (spawn call_once) (fn(E; fty) → join_handle retty).
   Proof.
     intros Hf ? E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
diff --git a/theories/typing/product.v b/theories/typing/product.v
index ccc7ba4783ca1b9a76ece9adffa192a8157362e4..fc4a8d9af4cc7aa65d554d13d64c277fbe2d592c 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -156,7 +156,7 @@ Section product.
   Definition unit := product [].
 
   Global Instance product_wf tyl `{!TyWfLst tyl} : TyWf (product tyl) :=
-    { ty_lfts := tyl.(tyl_lfts); ty_wf_E := tyl.(tyl_wf_E) }.
+    { ty_lfts := tyl_lfts tyl; ty_wf_E := tyl_wf_E tyl }.
 
   Lemma outlives_product ty1 ty2 ϝ `{!TyWf ty1, !TyWf ty2} :
     ty_outlives_E (product [ty1; ty2]) ϝ = ty_outlives_E ty1 ϝ ++ ty_outlives_E ty2 ϝ.
diff --git a/theories/typing/shr_bor.v b/theories/typing/shr_bor.v
index 7d8363539cdfedd3b32561adc9c251b64079fc20..b3a58cbf69bc02be96e2b7b3723c217666c9a9f9 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.(ty_outlives_E) κ }.
+    { ty_lfts := [κ]; ty_wf_E := ty.(ty_wf_E) ++ 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/sum.v b/theories/typing/sum.v
index 274a18038504b6d41757f40f3bff1a2ea5c99ed8..33c31594e7279e656f7d29a4574da67562f5b030 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -84,7 +84,7 @@ Section sum.
   Qed.
 
   Global Instance sum_wf tyl `{!TyWfLst tyl} : TyWf (sum tyl) :=
-    { ty_lfts := tyl.(tyl_lfts); ty_wf_E := tyl.(tyl_wf_E) }.
+    { ty_lfts := tyl_lfts tyl; ty_wf_E := tyl_wf_E tyl }.
 
   Global Instance sum_type_ne n : Proper (Forall2 (type_dist2 n) ==> type_dist2 n) sum.
   Proof.
diff --git a/theories/typing/type.v b/theories/typing/type.v
index c6b5bd7f5d74bb98b0a313347ad974111e31293f..5366feb1cb80ab9e45d52cb5129187fb1b9d6a20 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -63,9 +63,9 @@ Definition ty_outlives_E `{typeG Σ} ty `{!TyWf ty} (κ : lft) : elctx :=
   (λ α, κ ⊑ₑ α) <$> ty.(ty_lfts).
 
 Lemma ty_outlives_E_elctx_sat `{typeG Σ} E L ty `{!TyWf ty} α β :
-  ty.(ty_outlives_E) β ⊆+ E →
+  ty_outlives_E ty β ⊆+ E →
   lctx_lft_incl E L α β →
-  elctx_sat E L (ty.(ty_outlives_E) α).
+  elctx_sat E L (ty_outlives_E ty α).
 Proof.
   unfold ty_outlives_E. induction ty.(ty_lfts) as [|κ l IH]=>/= Hsub Hαβ.
   - solve_typing.
@@ -99,14 +99,14 @@ Fixpoint tyl_wf_E `{typeG Σ} tyl {WF : TyWfLst tyl} : elctx :=
 Fixpoint tyl_outlives_E `{typeG Σ} tyl {WF : TyWfLst tyl} (κ : lft) : elctx :=
   match WF with
   | tyl_wf_nil => []
-  | tyl_wf_cons ty [] => ty.(ty_outlives_E) κ
-  | tyl_wf_cons ty tyl => ty.(ty_outlives_E) κ ++ tyl.(tyl_outlives_E) κ
+  | tyl_wf_cons ty [] => ty_outlives_E ty κ
+  | tyl_wf_cons ty tyl => ty_outlives_E ty κ ++ tyl.(tyl_outlives_E) κ
   end.
 
 Lemma tyl_outlives_E_elctx_sat `{typeG Σ} E L tyl {WF : TyWfLst tyl} α β :
-  tyl.(tyl_outlives_E) β ⊆+ E →
+  tyl_outlives_E tyl β ⊆+ E →
   lctx_lft_incl E L α β →
-  elctx_sat E L (tyl.(tyl_outlives_E) α).
+  elctx_sat E L (tyl_outlives_E tyl α).
 Proof.
   induction WF as [|? [] ?? IH]=>/=.
   - solve_typing.
diff --git a/theories/typing/typing.v b/theories/typing/typing.v
index 6176df3a3a8d313f7838c5dc346c932626b7000f..ea4c662d2b558537318526dcb92b2b4bf6b46569 100644
--- a/theories/typing/typing.v
+++ b/theories/typing/typing.v
@@ -5,5 +5,5 @@ From lrust.typing Require Export
   product_split borrow type_sum.
 
 (* Last, so that we make sure we shadow the definition of delete for
-   collections coming from the prelude. *)
+   sets coming from the prelude. *)
 From lrust.lang Require Export new_delete.
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index 9178607453d2fcfd1b06ed86292b6aa934412148..0e59532a02f8fab2ec580fda5445eb8e39ed0d51 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.(ty_outlives_E) κ }.
+    { ty_lfts := [κ]; ty_wf_E := ty.(ty_wf_E) ++ ty_outlives_E ty κ }.
 
   Global Instance uniq_mono E L :
     Proper (flip (lctx_lft_incl E L) ==> eqtype E L ==> subtype E L) uniq_bor.