diff --git a/theories/examples/par.v b/theories/examples/par.v
index b3abcdefdf7368852cc291ae9fb8a31c0f46654c..da0301516055a637ced01aae0207c77a79b02e57 100644
--- a/theories/examples/par.v
+++ b/theories/examples/par.v
@@ -216,7 +216,7 @@ Section rules.
       iMod ("Hb" with "Hs Hi") as "Hb".
       iApply (wp_wand with "Hb").
       iIntros (bv). iDestruct 1 as (bv') "[Hi HB]". simpl.
-      wp_pures. wp_bind (join _).
+      wp_pures. wp_bind (spawn.join _).
       iApply (join_spec with "Hdl").
       iNext. iIntros (av). iDestruct 1 as (av') "[Hj HA]".
       wp_pures.
@@ -244,7 +244,7 @@ Section rules.
       wp_pures. iExists (cv', dv')%V. simpl.
       tp_pure i (InjR _). tp_store i.
       tp_pure j (Lam _ _). tp_pure j _. simpl.
-      rewrite /join. tp_pure j (App _ #c2). simpl.
+      rewrite /spawn.join. tp_pure j (App _ #c2). simpl.
       tp_load j. tp_case j. simpl.
       tp_pure j (Lam _ _). tp_pure j (App _ cv'). simpl.
       tp_pure j (Lam _ _). tp_pure j (App _ cv'). simpl.
diff --git a/theories/lib/lock.v b/theories/lib/lock.v
index a246d5681c9d46b9994f167848338cbd5ea80a88..f44599138b265266fb47deb28e15bde6fefd97ea 100644
--- a/theories/lib/lock.v
+++ b/theories/lib/lock.v
@@ -1,5 +1,5 @@
-From reloc Require Export reloc.
 From iris.algebra Require Import excl.
+From reloc Require Export reloc.
 Set Default Proof Using "Type".
 
 
diff --git a/theories/prelude/ctx_subst.v b/theories/prelude/ctx_subst.v
index ce998bdf4f8fd5be4ecbb7be8c208e5c5f4a1c0c..a8f2b6794b99adf10c105a65025b11eee1942f84 100644
--- a/theories/prelude/ctx_subst.v
+++ b/theories/prelude/ctx_subst.v
@@ -1,6 +1,6 @@
+From stdpp Require Import base stringmap fin_sets fin_map_dom.
 From iris.program_logic Require Export ectx_language ectxi_language.
 From iris.heap_lang Require Export lang metatheory.
-From stdpp Require Import base stringmap fin_sets fin_map_dom.
 
 (** Substitution in the contexts *)
 Fixpoint subst_map_ctx_item (es : stringmap val) (K : ectx_item)
diff --git a/theories/typing/fundamental.v b/theories/typing/fundamental.v
index 27e88df6b850cd4d2b253fc69f543f37f8c7376c..0ef44e018b82cf1bfba17a04ff8d95d10d7e032a 100644
--- a/theories/typing/fundamental.v
+++ b/theories/typing/fundamental.v
@@ -1,12 +1,11 @@
 (* ReLoC -- Relational logic for fine-grained concurrency *)
 (** Compatibility lemmas for the logical relation *)
+From Autosubst Require Import Autosubst.
 From iris.heap_lang Require Import proofmode.
 From reloc.logic Require Import model.
 From reloc.logic Require Export rules derived compatibility proofmode.tactics.
 From reloc.typing Require Export interp.
-
 From iris.proofmode Require Export tactics.
-From Autosubst Require Import Autosubst.
 
 Section fundamental.
   Context `{relocG Σ}.
@@ -450,7 +449,7 @@ Section fundamental.
     ({Δ;Γ} ⊨ e1 ≤log≤ e1' : ∃: τ) -∗
     (∀ τi : lrel Σ,
       {τi::Δ;<[x:=τ]>(⤉Γ)} ⊨
-        e2 ≤log≤ e2' : (subst (ren (+1)%nat) τ2)) -∗
+        e2 ≤log≤ e2' : (Autosubst_Classes.subst (ren (+1)%nat) τ2)) -∗
     {Δ;Γ} ⊨ (unpack: x := e1 in e2) ≤log≤ (unpack: x := e1' in e2') : τ2.
   Proof.
     iIntros "IH1 IH2".