diff --git a/opam b/opam
index 4ca4f67904479698624c19a2f67247967e452bb9..5e63a3dd15ff2e59ff5315b94deeb0d0f0dcad18 100644
--- a/opam
+++ b/opam
@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/reloc"]
 depends: [
-  "coq-iris" { (= "dev.2020-05-26.1.d80e7abf") | (= "dev") }
+  "coq-iris" { (= "dev.2020-05-28.3.38f177d3") | (= "dev") }
   "coq-autosubst" { = "dev.coq86" }
 ]
diff --git a/theories/examples/cell.v b/theories/examples/cell.v
index 38f290f2ce4444f2ff4f3acdbfef007ca579b05e..9936ba5299b44764731fdbdece2034eb4ffe7107 100644
--- a/theories/examples/cell.v
+++ b/theories/examples/cell.v
@@ -7,9 +7,9 @@ From reloc.lib Require Export lock.
 (** A type of cells -- basically an abstract type of references. *)
 (* ∀ α, ∃ β, (α → β) × (β → α) × (β → α → ())  *)
 Definition cellτ : type :=
-  ∀: ∃: (TVar 1%nat → TVar 0%nat)
-       * (TVar 0%nat → TVar 1%nat)
-       * (TVar 0%nat → TVar 1%nat → TUnit).
+  ∀: ∃: (TVar 1 → TVar 0)
+       * (TVar 0 → TVar 1)
+       * (TVar 0 → TVar 1 → TUnit).
 (** We show that the canonical implementation `cell1` is equivalent to
 an implementation using two alternating slots *)
 
diff --git a/theories/examples/namegen.v b/theories/examples/namegen.v
index 0694e940832f20f0c30b5822e653d4437828690b..aa759d1a2e774020f14bddc442e11a25f2545f14 100644
--- a/theories/examples/namegen.v
+++ b/theories/examples/namegen.v
@@ -11,8 +11,8 @@ version uses integers. *)
 (*       ^ new name  ^                            *)
 (*                   | compare names for equality *)
 Definition nameGenTy : type :=
-  ∃: (TUnit → TVar 0%nat)
-   * (TVar 0%nat → TVar 0%nat → TBool).
+  ∃: (TUnit → TVar 0)
+   * (TVar 0 → TVar 0 → TBool).
 
 (* TODO: cannot be a value *)
 Definition nameGen1 : expr :=
@@ -35,7 +35,7 @@ Section namegen_refinement.
     (∃ (n : nat) (L : gset (loc * nat)),
         BIJ γ L ∗ c ↦ₛ #n
      ∗  [∗ set] lk ∈ L, match lk with
-                        | (l, k) => l ↦ #() ∗ ⌜k ≤ n⌝%nat
+                        | (l, k) => l ↦ #() ∗ ⌜k ≤ n⌝
                         end)%I.
 
   Lemma nameGen_ref1 :
@@ -46,7 +46,7 @@ Section namegen_refinement.
     iMod alloc_empty_bij as (γ) "HB".
     pose (N:=relocN.@"ng").
     iMod (inv_alloc N _ (ng_Inv γ c) with "[-]") as "#Hinv".
-    { iNext. iExists 0%nat, ∅. iFrame.
+    { iNext. iExists 0, ∅. iFrame.
       by rewrite big_sepS_empty. }
     iApply (refines_exists (ngR γ)).
     do 2 rel_pure_r.
@@ -82,7 +82,7 @@ Section namegen_refinement.
         intros [l x] Hlx. apply bi.sep_mono_r, bi.pure_mono. lia. }
       rel_values. iModIntro.
       replace (Z.of_nat n + 1)%Z with (Z.of_nat (S n)); last lia.
-      iExists l', (S n)%nat; eauto.
+      iExists l', (S n); eauto.
     - (* Name comparison *)
       rel_pure_l. rel_pure_r.
       iApply refines_arrow_val.
diff --git a/theories/examples/or.v b/theories/examples/or.v
index 5ce043a9366f6a899aa865e22120d6f550d5e1e0..2b70b286f999102119bac2c93e1e05d127e9781b 100644
--- a/theories/examples/or.v
+++ b/theories/examples/or.v
@@ -325,12 +325,12 @@ Proof.
           + econstructor; cbn; eauto.
             econstructor; cbn; eauto.
             econstructor; cbn; eauto.
-            change Z0 with (Z.of_nat 0%nat).
+            change Z0 with (Z.of_nat 0).
             econstructor; cbn; eauto.
             econstructor; cbn; eauto.
             * econstructor; cbn; eauto.
               eapply Seq_typed.
-              ** change 1%Z with (Z.of_nat 1%nat).
+              ** change 1%Z with (Z.of_nat 1).
                  repeat (econstructor; cbn; eauto).
               ** repeat (econstructor; cbn; eauto).
             * repeat (econstructor; cbn; eauto).
diff --git a/theories/examples/symbol.v b/theories/examples/symbol.v
index d136a7e04a956ef93c22e737050bcbb6ae1e1bad..5d173f287230d62481ad7f9a1e5e9a3fd91b304f 100644
--- a/theories/examples/symbol.v
+++ b/theories/examples/symbol.v
@@ -60,7 +60,7 @@ Section rules.
   Lemma size_le (n m : nat) :
     own γ (● (n : mnat)) -∗
     own γ (◯ (m : mnat)) -∗
-    ⌜m ≤ n⌝%nat.
+    ⌜m ≤ n⌝.
   Proof.
     iIntros "Hn Hm".
     by iDestruct (own_valid_2 with "Hn Hm")
@@ -225,7 +225,7 @@ Section proof.
     rel_alloc_r size2 as "[Hs2 Hs2']"; repeat rel_pure_r.
     rel_alloc_l tbl1 as "[Htbl1 Htbl1']"; repeat rel_pure_l.
     rel_alloc_r tbl2 as "[Htbl2 Htbl2']"; repeat rel_pure_r.
-    iMod (own_alloc (● (0%nat : mnat))) as (γ) "Ha".
+    iMod (own_alloc (● (0 : mnat))) as (γ) "Ha".
     { by apply auth_auth_valid. }
     iMod (inv_alloc sizeN _ (table_inv γ size1 size2 tbl1 tbl2) with "[Hs1 Hs2 Htbl1 Htbl2 Ha]") as "#Hinv".
     { iNext. iExists _,_. iFrame. iApply lrel_list_nil. }
@@ -233,7 +233,7 @@ Section proof.
     iIntros (l2) "Hl2". rel_pure_r. rel_pure_r.
     pose (N:=(relocN.@"lock1")).
     rel_apply_l (refines_newlock_l N (lok_inv size1 size2 tbl1 tbl2 l2)%I with "[Hs1' Hs2' Htbl1' Htbl2' Hl2]").
-    { iExists 0%nat,_. by iFrame. }
+    { iExists 0,_. by iFrame. }
     iNext. iIntros (l1 γl) "#Hl1". rel_pure_l. rel_pure_l.
     iApply (refines_exists (tableR γ)).
     repeat iApply refines_pair.
@@ -304,7 +304,7 @@ Section proof.
     rel_alloc_r size2 as "[Hs2 Hs2']"; repeat rel_pure_r.
     rel_alloc_l tbl1 as "[Htbl1 Htbl1']"; repeat rel_pure_l.
     rel_alloc_r tbl2 as "[Htbl2 Htbl2']"; repeat rel_pure_r.
-    iMod (own_alloc (● (0%nat : mnat))) as (γ) "Ha".
+    iMod (own_alloc (● (0 : mnat))) as (γ) "Ha".
     { by apply auth_auth_valid. }
     iMod (inv_alloc sizeN _ (table_inv γ size1 size2 tbl1 tbl2) with "[Hs1 Hs2 Htbl1 Htbl2 Ha]") as "#Hinv".
     { iNext. iExists _,_. iFrame. iApply lrel_list_nil. }
@@ -312,7 +312,7 @@ Section proof.
     iIntros (l2) "Hl2". rel_pure_r. rel_pure_r.
     pose (N:=(relocN.@"lock1")).
     rel_apply_l (refines_newlock_l N (lok_inv size1 size2 tbl1 tbl2 l2)%I with "[Hs1' Hs2' Htbl1' Htbl2' Hl2]").
-    { iExists 0%nat,_. by iFrame. }
+    { iExists 0,_. by iFrame. }
     iNext. iIntros (l1 γl) "#Hl1". rel_pure_l. rel_pure_l.
     iApply (refines_exists (tableR γ)).
     repeat iApply refines_pair.
diff --git a/theories/examples/ticket_lock.v b/theories/examples/ticket_lock.v
index edecad12d161da8888a2e133241b5d3dbc952f83..3230b987cf3cb4fce6ccd94158d3f1f3a167865d 100644
--- a/theories/examples/ticket_lock.v
+++ b/theories/examples/ticket_lock.v
@@ -118,7 +118,7 @@ Section refinement.
     (* Establishing the invariant *)
     iMod newIssuedTickets as (γ) "Hγ".
     iMod (inv_alloc N _ (lockInv lo ln γ l') with "[-]") as "#Hinv".
-    { iNext. iExists 0%nat,0%nat,_. by iFrame. }
+    { iNext. iExists 0,0,_. by iFrame. }
     rel_pure_l.
     rel_values.
     iExists _,_,_. iFrame "Hinv". eauto.
@@ -335,8 +335,8 @@ Section refinement.
       iIntros "Hl'".
       iMod ("Hcl" with "[-]") as "_".
       { iNext.
-        replace (o' + 1)%Z with (Z.of_nat (o' + 1))%nat by lia.
-        iExists (o' + 1)%nat,_,_. by iFrame. }
+        replace (o' + 1)%Z with (Z.of_nat (o' + 1)) by lia.
+        iExists (o' + 1),_,_. by iFrame. }
       rel_values.
   Qed.
 
diff --git a/theories/examples/various.v b/theories/examples/various.v
index d986b6337d0c3162847e4ff1c4d714383288a5e6..146fdeef4127b1c61b141e4e07ea6e20df570d7c 100644
--- a/theories/examples/various.v
+++ b/theories/examples/various.v
@@ -190,7 +190,7 @@ Section proofs.
     rel_alloc_r x' as "Hx'".
     rel_pure_r. rel_pure_r.
     iMod (inv_alloc i3n _ (i3 x x' b b') with "[-]") as "#Hinv".
-    { iNext. unfold i3. iExists 0%nat.
+    { iNext. unfold i3. iExists 0.
       iDestruct "Hx" as "[$ Hx]".
       iDestruct "Hx'" as "[$ Hx']".
       iLeft. iFrame. }
@@ -388,7 +388,7 @@ Section proofs.
       { iIntros "[Hc1 [(Hc2 & Ht) | (Hc2 & Ht & Ht' & %)]]";
         iApply ("Hcl" with "[-]"); iNext.
         + iExists n. iLeft. iFrame.
-        + iExists (n-1)%nat. iRight.
+        + iExists (n-1). iRight.
           replace (Z.of_nat (n - 1)) with (Z.of_nat n - 1)%Z by lia.
           replace (n - 1 + 1)%Z with (Z.of_nat n) by lia.
          iFrame. }
@@ -396,7 +396,7 @@ Section proofs.
         iDestruct "Hc" as "[[Hc2 Ht] | [Hc2 [Ht [Ht' %]]]]".
         - rel_apply_r (FG_increment_r with "Hc2"). iIntros "Hc2".
           iMod ("Hcl" with "[-]") as "_".
-          { iNext. iExists (n + 1)%nat.
+          { iNext. iExists (n + 1).
             replace (Z.of_nat (n + 1)) with (Z.of_nat n + 1)%Z by lia.
             iLeft; iFrame. }
           rel_values.
@@ -406,7 +406,7 @@ Section proofs.
           { iNext. iExists n. iRight; iFrame.
             by replace ((n - 1)%nat + 1)%Z with (Z.of_nat n) by lia. }
          rel_values. }
-    - iModIntro. iExists (n + 1)%nat.
+    - iModIntro. iExists (n + 1).
       replace (Z.of_nat n + 1)%Z with (Z.of_nat (n + 1)) by lia. iFrame.
       iSplitL "Hc2 Ht".
       { iRight. replace ((n + 1)%nat - 1)%Z with (Z.of_nat n) by lia.
@@ -463,7 +463,7 @@ Section proofs.
   Proof.
     iDestruct 1 as (m) "[Hc1 Hc2]".
     iDestruct "Hc2" as "[[Hc2 Hp] | (Hc2 & Hs & Ht & %)]";
-      [iExists m; iLeft | iExists (m - 1)%nat; iRight]; iFrame.
+      [iExists m; iLeft | iExists (m - 1); iRight]; iFrame.
     replace ((m - 1)%nat + 1)%Z with (Z.of_nat m) by lia.
     replace (Z.of_nat (m - 1)) with (Z.of_nat m - 1)%Z by lia.
     iFrame.
@@ -540,7 +540,7 @@ Section proofs.
     iMod new_pending as (γ) "Ht".
     iMod (own_alloc (Excl ())) as (γ') "Ht'"; first done.
     iMod (inv_alloc shootN _ (i6 c1 c2 γ γ') with "[Hc1 Hc2 Ht]") as "#Hinv".
-    { iNext. iExists 0%nat. iLeft. iFrame. }
+    { iNext. iExists 0. iLeft. iFrame. }
     repeat rel_pure_l. repeat rel_pure_r.
     iApply (refines_seq lrel_unit).
     { iApply (refines_app with "Hf").
diff --git a/theories/experimental/helping/offers.v b/theories/experimental/helping/offers.v
index 7403f5fae29fcccf6bb41beeb6a7e32a84b2af24..2bb656743ce858876c2b27857fcb89dc58a5a566 100644
--- a/theories/experimental/helping/offers.v
+++ b/theories/experimental/helping/offers.v
@@ -70,7 +70,7 @@ Section rules.
       rel_pures_l. iApply ("Hcont" with "[-]").
       iExists _; iFrame.
     - iIntros (?). simplify_eq/=.
-      assert (c = 0%nat) as -> by lia. (* :) *)
+      assert (c = 0) as -> by lia. (* :) *)
       iNext. iIntros "Hl".
       iDestruct "Hoff" as "[[% HP] | [[% ?] | [% ?]]]"; [| congruence..].
       rel_pures_l.
diff --git a/theories/experimental/hocap/counter.v b/theories/experimental/hocap/counter.v
index 37a1839a82391b2142d5d74e56647f431d8a421a..ba83aad29540f17f8cc48002d4be422744fad188 100644
--- a/theories/experimental/hocap/counter.v
+++ b/theories/experimental/hocap/counter.v
@@ -280,7 +280,7 @@ Section refinement.
     iIntros "Hl Hlk".
     iMod ("Hcl" with "[-]") as "_".
     { iNext. iExists (n+1); try iFrame.
-      assert (Z.of_nat (n + 1)%nat = Z.of_nat n + 1)%Z as -> by lia.
+      assert (Z.of_nat (n + 1) = Z.of_nat n + 1)%Z as -> by lia.
       done. }
     rel_values.
   Qed.
@@ -317,12 +317,12 @@ Section refinement.
     rel_alloc_r c' as "Hcnt'".
     rel_alloc_l c as "Hcnt". simpl.
 
-    iMod (Cnt_alloc N _ 0%nat with "Hcnt") as (γ) "[#HCnt Hc]".
+    iMod (Cnt_alloc N _ 0 with "Hcnt") as (γ) "[#HCnt Hc]".
 
     (* establishing the invariant *)
     iMod (inv_alloc N2 _ (∃ m, is_locked_r lk false ∗ cnt γ 1 m ∗ c' ↦ₛ #m)%I
          with "[-]") as "#Hinv".
-    { iNext. iExists 0%nat. by iFrame. }
+    { iNext. iExists 0. by iFrame. }
     (* TODO: here we have to do /exactly/ 4 steps.
        The next step will reduce `(Val v1, Val v2)` to `Val (v1, v2)`,
        and the compatibility rule wouldn't be applicable *)
diff --git a/theories/experimental/hocap/ticket_lock.v b/theories/experimental/hocap/ticket_lock.v
index d0f20588f38fce80d634fc5deaf1004c5e58e3c0..2aa85b9594a3dbca75cd1897286f895ba0a644c2 100644
--- a/theories/experimental/hocap/ticket_lock.v
+++ b/theories/experimental/hocap/ticket_lock.v
@@ -117,7 +117,7 @@ Section refinement.
     iMod (Cnt_alloc (N.@"cnt1") _ 0 with "Hlo") as (γlo) "[#Hc2 Hlo]".
     iMod newIssuedTickets as (γ) "Hγ".
     iMod (inv_alloc (N.@"lock") _ (lockInv γln γlo γ l') with "[-]") as "#Hinv".
-    { iNext. iExists 0%nat,0%nat,_. iFrame. }
+    { iNext. iExists 0,0,_. iFrame. }
     rel_values. iModIntro. iExists _,_,_,_,_. iSplit; eauto with iFrame.
   Qed.
 
diff --git a/theories/logic/adequacy.v b/theories/logic/adequacy.v
index bb0ac2a59b6e1a23be73541b01c210117b418388..e82a01f1b6df82dd4d9da16dc53622a3fe012cbb 100644
--- a/theories/logic/adequacy.v
+++ b/theories/logic/adequacy.v
@@ -44,7 +44,7 @@ Proof.
   - iPoseProof (Hlog _) as "Hrel".
     rewrite refines_eq /refines_def /spec_ctx.
     iApply fupd_wp.
-    iSpecialize ("Hrel" $! 0%nat [] with "[Hcfg]"); first by eauto.
+    iSpecialize ("Hrel" $! 0 [] with "[Hcfg]"); first by eauto.
     iApply "Hrel".
     rewrite tpool_mapsto_eq /tpool_mapsto_def. iFrame.
     by rewrite /to_tpool /= insert_empty map_fmap_singleton //.
diff --git a/theories/logic/proofmode/tactics.v b/theories/logic/proofmode/tactics.v
index 3f2efedb518040ead1d80c86622907bd75169226..54ea266baf9fdb49ef38f3029300e512bd5899bb 100644
--- a/theories/logic/proofmode/tactics.v
+++ b/theories/logic/proofmode/tactics.v
@@ -128,7 +128,7 @@ Lemma tac_rel_pure_l `{!relocG Σ} K e1 ℶ ℶ' E e e2 eres ϕ n m t A :
   e = fill K e1 →
   PureExec ϕ n e1 e2 →
   ϕ →
-  ((m = n ∧ E = ⊤) ∨ m = 0%nat) →
+  ((m = n ∧ E = ⊤) ∨ m = 0) →
   MaybeIntoLaterNEnvs m ℶ ℶ' →
   eres = fill K e2 →
   envs_entails ℶ' (REL eres << t @ E : A) →
diff --git a/theories/logic/spec_rules.v b/theories/logic/spec_rules.v
index f22546c9b4cb126abfb0a2ffda1057021ded4688..be1abfca329b4137f65afff93861039361b7e5e2 100644
--- a/theories/logic/spec_rules.v
+++ b/theories/logic/spec_rules.v
@@ -327,7 +327,7 @@ Section rules.
     iInv specN as (tp σ) ">[Hown %]" "Hclose".
     iDestruct (own_valid_2 with "Hown Hj")
       as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_both_valid.
-    assert (j < length tp)%nat by eauto using lookup_lt_Some.
+    assert (j < length tp) by eauto using lookup_lt_Some.
     iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
     { by eapply auth_update, prod_local_update_1,
         singleton_local_update, (exclusive_local_update _ (Excl (fill K #()))). }
diff --git a/theories/typing/contextual_refinement.v b/theories/typing/contextual_refinement.v
index 74c7248b207387bdcca2c13888a4026033f85986..ea12f0ce5914520bddf54d3ca1c6d95858fb1403 100644
--- a/theories/typing/contextual_refinement.v
+++ b/theories/typing/contextual_refinement.v
@@ -203,18 +203,18 @@ Inductive typed_ctx_item :
   | TP_CTX_Unfold Γ τ :
      typed_ctx_item CTX_Unfold Γ (TRec τ) Γ τ.[(TRec τ)/]
   | TP_CTX_TLam Γ τ :
-     typed_ctx_item CTX_TLam (Autosubst_Classes.subst (ren (+1%nat)) <$> Γ) τ Γ (TForall τ)
+     typed_ctx_item CTX_TLam (Autosubst_Classes.subst (ren (+1)) <$> Γ) τ Γ (TForall τ)
   | TP_CTX_TApp Γ τ τ' :
      typed_ctx_item CTX_TApp Γ (TForall τ) Γ τ.[τ'/]
   (* | TP_CTX_Pack Γ τ τ' : *)
   (*    typed_ctx_item CTX_Pack Γ τ.[τ'/] Γ (TExists τ) *)
   | TP_CTX_UnpackL x e2 Γ τ τ2 :
-     <[x:=τ]>(⤉ Γ) ⊢ₜ e2 : (Autosubst_Classes.subst (ren (+1%nat)) τ2) →
+     <[x:=τ]>(⤉ Γ) ⊢ₜ e2 : (Autosubst_Classes.subst (ren (+1)) τ2) →
      typed_ctx_item (CTX_UnpackL x e2) Γ (TExists τ) Γ τ2
   | TP_CTX_UnpackR x e1 Γ τ τ2 :
       Γ ⊢ₜ e1 : TExists τ →
      typed_ctx_item (CTX_UnpackR x e1)
-                    (<[x:=τ]>(⤉ Γ)) (Autosubst_Classes.subst (ren (+1%nat)) τ2)
+                    (<[x:=τ]>(⤉ Γ)) (Autosubst_Classes.subst (ren (+1)) τ2)
                     Γ τ2
 .
 
diff --git a/theories/typing/fundamental.v b/theories/typing/fundamental.v
index 74d4d01800a09d9d3cea6cd26e065431ed2127ca..2eec8e2cfe9c2a6166ef252b84c5e03fc9fb9ceb 100644
--- a/theories/typing/fundamental.v
+++ b/theories/typing/fundamental.v
@@ -194,7 +194,7 @@ Section fundamental.
     {Δ;Γ} ⊨ (e1;; e2) ≤log≤ (e1';; e2') : τ2.
   Proof.
     iIntros "He1 He2".
-    iApply (bin_log_related_seq lrel_true _ _ _ _ _ _ Ï„1.[ren (+1)%nat] with "[He1] He2").
+    iApply (bin_log_related_seq lrel_true _ _ _ _ _ _ Ï„1.[ren (+1)] with "[He1] He2").
     intro_clause.
     rewrite interp_ren -(interp_ren_up [] Δ τ1).
     by iApply "He1".
@@ -472,7 +472,7 @@ Section fundamental.
     ({Δ;Γ} ⊨ e1 ≤log≤ e1' : ∃: τ) -∗
     (∀ τi : lrel Σ,
       {τi::Δ;<[x:=τ]>(⤉Γ)} ⊨
-        e2 ≤log≤ e2' : (Autosubst_Classes.subst (ren (+1)%nat) τ2)) -∗
+        e2 ≤log≤ e2' : (Autosubst_Classes.subst (ren (+1)) τ2)) -∗
     {Δ;Γ} ⊨ (unpack: x := e1 in e2) ≤log≤ (unpack: x := e1' in e2') : τ2.
   Proof.
     iIntros "IH1 IH2".
diff --git a/theories/typing/interp.v b/theories/typing/interp.v
index 2845ffcf974a91657c318d4ea695e8045046ce76..7f52e376329bbf7a4d6a00526257c18a0d602142 100644
--- a/theories/typing/interp.v
+++ b/theories/typing/interp.v
@@ -83,7 +83,7 @@ Section interp_ren.
 
   (* TODO: why do I need to unfold lrel_car here? *)
   Lemma interp_ren_up (Δ1 Δ2 : list (lrel Σ)) τ τi :
-    interp τ (Δ1 ++ Δ2) ≡ interp (τ.[upn (length Δ1) (ren (+1)%nat)]) (Δ1 ++ τi :: Δ2).
+    interp τ (Δ1 ++ Δ2) ≡ interp (τ.[upn (length Δ1) (ren (+1))]) (Δ1 ++ τi :: Δ2).
   Proof.
     revert Δ1 Δ2. induction τ => Δ1 Δ2; simpl; eauto;
     try by
@@ -96,7 +96,7 @@ Section interp_ren.
       { by rewrite !lookup_app_l. }
       change (bi_ofeO (uPredI (iResUR Σ))) with (uPredO (iResUR Σ)).
       rewrite !lookup_app_r; [|lia..].
-      assert ((length Δ1 + S (x - length Δ1) - length Δ1) = S (x - length Δ1))%nat as Hwat.
+      assert ((length Δ1 + S (x - length Δ1) - length Δ1) = S (x - length Δ1)) as Hwat.
       { lia. }
       rewrite Hwat. simpl. done.
     - intros v1 v2; unfold lrel_car; simpl;
@@ -151,7 +151,7 @@ Section interp_ren.
       rewrite iter_up; case_decide; simpl; properness.
       { by rewrite !lookup_app_l. }
       rewrite !lookup_app_r; [|lia..].
-      case EQ: (x - length Δ1)%nat => [|n]; simpl.
+      case EQ: (x - length Δ1)=> [|n]; simpl.
       { symmetry.
         pose (HW := interp_weaken [] Δ1 Δ2 τ' w1 w2).
         etrans; last by apply HW.
diff --git a/theories/typing/types.v b/theories/typing/types.v
index c94c6d6c02f748c6b0f4231415d6b07173ceafcf..a3c6ded9760d8d9a8c2b4b33605f46f3eaf6d0f1 100644
--- a/theories/typing/types.v
+++ b/theories/typing/types.v
@@ -76,7 +76,7 @@ Reserved Notation "⊢ᵥ v : τ" (at level 20, v, τ at next level).
 
 (* Shift all the indices in the context by one,
    used when inserting a new type interpretation in Δ. *)
-Notation "⤉ Γ" := (Autosubst_Classes.subst (ren (+1)%nat) <$> Γ) (at level 10, format "⤉ Γ").
+Notation "⤉ Γ" := (Autosubst_Classes.subst (ren (+1)) <$> Γ) (at level 10, format "⤉ Γ").
 
 (** We model type-level lambdas and applications as thunks *)
 Notation "Λ: e" := (λ: <>, e)%E (at level 200, only parsing).
@@ -172,7 +172,7 @@ Inductive typed : stringmap type → expr → type → Prop :=
       Γ ⊢ₜ e : (∃: τ)
   | TUnpack Γ e1 x e2 τ τ2 :
       Γ ⊢ₜ e1 : (∃: τ) →
-      <[x:=τ]>(⤉ Γ) ⊢ₜ e2 : (Autosubst_Classes.subst (ren (+1%nat)) τ2) →
+      <[x:=τ]>(⤉ Γ) ⊢ₜ e2 : (Autosubst_Classes.subst (ren (+1)) τ2) →
       Γ ⊢ₜ (unpack: x := e1 in e2) : τ2
   | TFork Γ e : Γ ⊢ₜ e : TUnit → Γ ⊢ₜ Fork e : TUnit
   | TAlloc Γ e τ : Γ ⊢ₜ e : τ → Γ ⊢ₜ Alloc e : Tref τ