diff --git a/semantics.opam b/semantics.opam
index 90fbb39e32d712bf1e654889da87abff7d434af3..b2637665bf0ab879e270a38179b0a4e74232977d 100644
--- a/semantics.opam
+++ b/semantics.opam
@@ -12,7 +12,7 @@ depends: [
   "coq" { (>= "8.13" & < "8.17~") | (= "dev") }
   "coq-iris-heap-lang" { (= "dev.2022-09-21.1.291dc89e") | (= "dev") }
   "coq-equations" { (= "1.2.4+8.13") | (= "1.3+8.14") | (= "1.3+8.15")  | (= "1.3+8.16") }
-  "coq-autosubst" { = "1.7" }
+  "coq-autosubst" { (= "1.7") | (= "dev")  }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/program_logics/concurrency.v b/theories/program_logics/concurrency.v
index 435a83470d44e08b73c0b7144550ab2d56944841..1c30fb7f3f7c7ce454d635d8adb85c6d063f5548 100644
--- a/theories/program_logics/concurrency.v
+++ b/theories/program_logics/concurrency.v
@@ -153,9 +153,9 @@ Section spin_lock.
 
   (** Lock specification *)
   Definition lockN : namespace := nroot .@ "lock".
-  Definition lock_inv l (P : iProp Σ) :=
+  Definition lock_inv (l : loc) (P : iProp Σ) : iProp Σ :=
     ((l ↦ #false ∗ P) ∨ (l ↦ #true))%I.
-  Definition is_lock v P :=
+  Definition is_lock (v : val) (P : iProp Σ) : iProp Σ :=
     (∃ l : loc, ⌜v = #l⌝ ∗ inv lockN (lock_inv l P))%I.
 
   Instance is_lock_pers v P : Persistent (is_lock v P).
@@ -262,8 +262,8 @@ End lock_lemmas.
 Section excl_spin_lock.
   Context `{heapGS Σ} `{lockG Σ}.
 
-  Definition is_excl_lock v γ P :=
-         is_lock v P 
+  Definition is_excl_lock (v : val) (γ : gname) (P : iProp Σ) : iProp Σ :=
+        is_lock v P (* TODO *)
   .
 
   Instance is_excl_lock_pers v γ  P : Persistent (is_excl_lock v γ P).
diff --git a/theories/type_systems/systemf/types.v b/theories/type_systems/systemf/types.v
index 7346fad9a44d3faa9b475f5bbe5e6f261d1093dc..d6ffb7e7deaa270d47b91da15851afc0f28e2008 100644
--- a/theories/type_systems/systemf/types.v
+++ b/theories/type_systems/systemf/types.v
@@ -275,7 +275,7 @@ Proof.
   induction 1 in δ |-*; intros Hmon; simpl; eauto.
   all: econstructor; eapply type_wf_mono; first eapply IHtype_wf; last done.
   all: intros i j Hlt; destruct i, j; simpl; try lia.
-  all: by eapply lt_n_S, Hmon, lt_S_n.
+  all: rewrite -Nat.succ_lt_mono; eapply Hmon; lia.
 Qed.
 
 (** [A.[σ]], i.e. [A] with the substitution [σ] applied to it, is well-formed under [m] if
@@ -290,12 +290,12 @@ Proof.
   + econstructor; eapply IHtype_wf.
     intros [|x]; rewrite /up //=.
     - econstructor. lia.
-    - intros Hlt % lt_S_n. eapply type_wf_rename; eauto.
+    - intros Hlt % Nat.succ_lt_mono. eapply type_wf_rename; eauto.
       intros i j Hlt'; simpl; lia.
   + econstructor; eapply IHtype_wf.
     intros [|x]; rewrite /up //=.
     - econstructor. lia.
-    - intros Hlt % lt_S_n. eapply type_wf_rename; eauto.
+    - intros Hlt % Nat.succ_lt_mono. eapply type_wf_rename; eauto.
       intros i j Hlt'; simpl; lia.
 Qed.
 
diff --git a/theories/type_systems/systemf_mu/types.v b/theories/type_systems/systemf_mu/types.v
index a8e88e62a36dc6bbf2a335c6ca35200ed1262d20..eaca72d9afbf83e92b19ec9b6ca1b0c56c347b10 100644
--- a/theories/type_systems/systemf_mu/types.v
+++ b/theories/type_systems/systemf_mu/types.v
@@ -288,7 +288,7 @@ Proof.
   induction 1 in δ |-*; intros Hmon; simpl; eauto.
   all: econstructor; eapply type_wf_mono; first eapply IHtype_wf; last done.
   all: intros i j Hlt; destruct i, j; simpl; try lia.
-  all: by eapply lt_n_S, Hmon, lt_S_n.
+  all: rewrite -Nat.succ_lt_mono; eapply Hmon; lia.
 Qed.
 
 (** [A.[σ]], i.e. [A] with the substitution [σ] applied to it, is well-formed under [m] if
@@ -303,17 +303,17 @@ Proof.
   + econstructor; eapply IHtype_wf.
     intros [|x]; rewrite /up //=.
     - econstructor. lia.
-    - intros Hlt % lt_S_n. eapply type_wf_rename; eauto.
+    - intros Hlt % Nat.succ_lt_mono. eapply type_wf_rename; eauto.
       intros i j Hlt'; simpl; lia.
   + econstructor; eapply IHtype_wf.
     intros [|x]; rewrite /up //=.
     - econstructor. lia.
-    - intros Hlt % lt_S_n. eapply type_wf_rename; eauto.
+    - intros Hlt % Nat.succ_lt_mono. eapply type_wf_rename; eauto.
       intros i j Hlt'; simpl; lia.
   + econstructor. eapply IHtype_wf.
     intros [|x]; rewrite /up //=.
     - econstructor. lia.
-    - intros Hlt % lt_S_n. eapply type_wf_rename; eauto.
+    - intros Hlt % Nat.succ_lt_mono. eapply type_wf_rename; eauto.
       intros ???. simpl; lia.
 Qed.
 
diff --git a/theories/type_systems/systemf_mu_state/logrel.v b/theories/type_systems/systemf_mu_state/logrel.v
index fccf98b842421525b37da86d50b298472f51eb8c..bc3afd733dc3e1d2f3838cdc3dc034ea85d30e5c 100644
--- a/theories/type_systems/systemf_mu_state/logrel.v
+++ b/theories/type_systems/systemf_mu_state/logrel.v
@@ -346,7 +346,7 @@ Proof.
   destruct Hincl as (W''& ->).
   exists (length W'' + i).
   rewrite lookup_app_r; last lia.
-  by rewrite minus_plus.
+  by rewrite Nat.add_comm Nat.add_sub.
 Qed.
 
 Lemma wsat_merge σ1 σ2 W1 W2 :
diff --git a/theories/type_systems/systemf_mu_state/types.v b/theories/type_systems/systemf_mu_state/types.v
index d1f982df4c8821061888ab16224f2955e1da7110..3f737074561b55fdd2111fa91f915ba13d603125 100644
--- a/theories/type_systems/systemf_mu_state/types.v
+++ b/theories/type_systems/systemf_mu_state/types.v
@@ -309,7 +309,7 @@ Proof.
   induction 1 in δ |-*; intros Hmon; simpl; eauto.
   all: econstructor; eapply type_wf_mono; first eapply IHtype_wf; last done.
   all: intros i j Hlt; destruct i, j; simpl; try lia.
-  all: by eapply lt_n_S, Hmon, lt_S_n.
+  all: rewrite -Nat.succ_lt_mono; eapply Hmon; lia.
 Qed.
 
 (** [A.[σ]], i.e. [A] with the substitution [σ] applied to it, is well-formed under [m] if
@@ -324,17 +324,17 @@ Proof.
   + econstructor; eapply IHtype_wf.
     intros [|x]; rewrite /up //=.
     - econstructor. lia.
-    - intros Hlt % lt_S_n. eapply type_wf_rename; eauto.
+    - intros Hlt % Nat.succ_lt_mono. eapply type_wf_rename; eauto.
       intros i j Hlt'; simpl; lia.
   + econstructor; eapply IHtype_wf.
     intros [|x]; rewrite /up //=.
     - econstructor. lia.
-    - intros Hlt % lt_S_n. eapply type_wf_rename; eauto.
+    - intros Hlt % Nat.succ_lt_mono. eapply type_wf_rename; eauto.
       intros i j Hlt'; simpl; lia.
   + econstructor. eapply IHtype_wf.
     intros [|x]; rewrite /up //=.
     - econstructor. lia.
-    - intros Hlt % lt_S_n. eapply type_wf_rename; eauto.
+    - intros Hlt % Nat.succ_lt_mono. eapply type_wf_rename; eauto.
       intros ???. simpl; lia.
 Qed.