diff --git a/CHANGELOG.md b/CHANGELOG.md
index b1c497ad9074d7af96463077776dc7eef00577ac..84c3259c05c85dc2efbd2ff3e69570e1a32421b6 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -198,6 +198,8 @@ Coq development, but not every API-breaking change is listed.  Changes marked
 * Add lemmas `inv_combine` and `inv_combine_dup_l` for combining invariants.
 * Rename `heap_lang.lifting` to `heap_lang.primitive_laws`. There now also
   exists `heap_lang.derived_laws`.
+* Remove global `Open Scope Z_scope` from `heap_lang.lang`, and leave it up to
+  reverse dependencies if they want to `Open Scope Z_scope` or not.
 
 The following `sed` script should perform most of the renaming (FIXME: incomplete)
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):
diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index 9fb599d4c42e6e27ba56f5f3866a577a28e7a963..4a40a842e1dc6d9daeb31cadbb0c8cf362a68285 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -90,7 +90,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
   Σ : gFunctors
   heapG0 : heapG Σ
   n : Z
-  H : 0 < n
+  H : (0 < n)%Z
   Φ : val → iPropI Σ
   l : loc
   ============================
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 5de009c350ace8a10aa6817c20fb7abb8b2f77d6..68bfa9ab21da4c5b67b150173a728d083815ea35 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -98,14 +98,14 @@ Section tests.
       if: "x" ≤ #0 then -FindPred (-"x" + #2) #0 else FindPred "x" #0.
 
   Lemma FindPred_spec n1 n2 E Φ :
-    n1 < n2 →
+    (n1 < n2)%Z →
     Φ #(n2 - 1) -∗ WP FindPred #n2 #n1 @ E [{ Φ }].
   Proof.
     iIntros (Hn) "HΦ".
     iInduction (Z.gt_wf n2 n1) as [n1' _] "IH" forall (Hn).
     wp_rec. wp_pures. case_bool_decide; wp_if.
     - iApply ("IH" with "[%] [%] HΦ"); lia.
-    - by assert (n1' = n2 - 1) as -> by lia.
+    - by assert (n1' = n2 - 1)%Z as -> by lia.
   Qed.
 
   Lemma Pred_spec n E Φ : Φ #(n - 1) -∗ WP Pred #n @ E [{ Φ }].
@@ -113,7 +113,7 @@ Section tests.
     iIntros "HΦ". wp_lam.
     wp_op. case_bool_decide.
     - wp_apply FindPred_spec; first lia. wp_pures.
-      by replace (n - 1) with (- (-n + 2 - 1)) by lia.
+      by replace (n - 1)%Z with (- (-n + 2 - 1))%Z by lia.
     - wp_apply FindPred_spec; eauto with lia.
   Qed.
 
@@ -130,12 +130,12 @@ Section tests.
   Lemma Id_wp (n : nat) : ⊢ WP Id #n {{ v, ⌜ v = #() ⌝ }}.
   Proof.
     iInduction n as [|n] "IH"; wp_rec; wp_pures; first done.
-    by replace (S n - 1) with (n:Z) by lia.
+    by replace (S n - 1)%Z with (n:Z) by lia.
   Qed.
   Lemma Id_twp (n : nat) : ⊢ WP Id #n [{ v, ⌜ v = #() ⌝ }].
   Proof.
     iInduction n as [|n] "IH"; wp_rec; wp_pures; first done.
-    by replace (S n - 1) with (n:Z) by lia.
+    by replace (S n - 1)%Z with (n:Z) by lia.
   Qed.
 
   Lemma wp_apply_evar e P :
@@ -162,20 +162,22 @@ Section tests.
     ⊢ WP let: "x" := #() in (λ: "y", "x")%V #() {{ _, True }}.
   Proof. wp_let. wp_lam. Fail wp_pure _. Show. Abort.
 
-  Lemma wp_alloc_array n : 0 < n →
+  Lemma wp_alloc_array n :
+    (0 < n)%Z →
     ⊢ {{{ True }}}
         AllocN #n #0
-      {{{ l, RET #l;  l ↦∗ replicate (Z.to_nat n) #0}}}.
+      {{{ l, RET #l;  l ↦∗ replicate (Z.to_nat n) #0 }}}.
   Proof.
     iIntros (? Φ) "!> _ HΦ".
     wp_alloc l as "?"; first done.
     by iApply "HΦ".
   Qed.
 
-  Lemma twp_alloc_array n : 0 < n →
+  Lemma twp_alloc_array n :
+    (0 < n)%Z →
     ⊢ [[{ True }]]
         AllocN #n #0
-      [[{ l, RET #l; l ↦∗ replicate (Z.to_nat n) #0}]].
+      [[{ l, RET #l; l ↦∗ replicate (Z.to_nat n) #0 }]].
   Proof.
     iIntros (? Φ) "!> _ HΦ".
     wp_alloc l as "?"; first done. Show.
diff --git a/tests/ipm_paper.v b/tests/ipm_paper.v
index 8539b5d44b81c6c73d4477c6b19891aa848b00d4..b3e0527dd0fad2378e97be5f101e57e5c51c04c3 100644
--- a/tests/ipm_paper.v
+++ b/tests/ipm_paper.v
@@ -137,7 +137,7 @@ Section M.
   Instance M_valid : Valid M := λ x, x ≠ Bot.
   Instance M_op : Op M := λ x y,
     match x, y with
-    | Auth n, Frag j | Frag j, Auth n => if decide (j ≤ n)%nat then Auth n else Bot
+    | Auth n, Frag j | Frag j, Auth n => if decide (j ≤ n) then Auth n else Bot
     | Frag i, Frag j => Frag (max i j)
     | _, _ => Bot
     end.
@@ -171,9 +171,9 @@ Section M.
 
   Global Instance frag_core_id n : CoreId (Frag n).
   Proof. by constructor. Qed.
-  Lemma auth_frag_valid j n : ✓ (Auth n ⋅ Frag j) → (j ≤ n)%nat.
+  Lemma auth_frag_valid j n : ✓ (Auth n ⋅ Frag j) → j ≤ n.
   Proof. simpl. case_decide. done. by intros []. Qed.
-  Lemma auth_frag_op (j n : nat) : (j ≤ n)%nat → Auth n = Auth n ⋅ Frag j.
+  Lemma auth_frag_op (j n : nat) : j ≤ n → Auth n = Auth n ⋅ Frag j.
   Proof. intros. by rewrite /= decide_True. Qed.
 
   Lemma M_update n : Auth n ~~> Auth (S n).
@@ -209,7 +209,7 @@ Section counter_proof.
     rewrite (auth_frag_op 0 0) //; iDestruct "Hγ" as "[Hγ Hγf]".
     set (N:= nroot .@ "counter").
     iMod (inv_alloc N _ (I γ l) with "[Hl Hγ]") as "#?".
-    { iIntros "!>". iExists 0%nat. by iFrame. }
+    { iIntros "!>". iExists 0. by iFrame. }
     iModIntro. rewrite /C; eauto 10.
   Qed.
 
diff --git a/tests/tree_sum.v b/tests/tree_sum.v
index e2406fac957f2ddf9a55e30525cf2ab92f748bf3..221e86d15cca55c51309d6eaece7a25ba935b1f9 100644
--- a/tests/tree_sum.v
+++ b/tests/tree_sum.v
@@ -48,7 +48,7 @@ Proof.
     wp_load. wp_apply ("IH" with "Hl Htl"). iIntros "[Hl Htl]".
     wp_load. wp_apply ("IH1" with "Hl Htr"). iIntros "[Hl Htr]".
     iApply "HΦ". iSplitL "Hl".
-    { by replace (sum tl + sum tr + n) with (sum tr + (sum tl + n)) by lia. }
+    { by replace (sum tl + sum tr + n)%Z with (sum tr + (sum tl + n))%Z by lia. }
     iExists ll, lr, vl, vr. by iFrame.
 Qed.
 
diff --git a/theories/heap_lang/derived_laws.v b/theories/heap_lang/derived_laws.v
index 1e36d1f7a9df0788677250eb80a308613c1bd529..c2aafac5b642f6d5e748a93c6694988b830f0667 100644
--- a/theories/heap_lang/derived_laws.v
+++ b/theories/heap_lang/derived_laws.v
@@ -78,7 +78,7 @@ Proof.
   rewrite -[X in (l ↦∗{_} X)%I](take_drop_middle _ off v); last done.
   iDestruct (array_app with "Hl") as "[Hl1 Hl]".
   iDestruct (array_cons with "Hl") as "[Hl2 Hl3]".
-  assert (off < length vs)%nat as H by (apply lookup_lt_is_Some; by eexists).
+  assert (off < length vs) as H by (apply lookup_lt_is_Some; by eexists).
   rewrite take_length min_l; last by lia. iFrame "Hl2".
   iIntros (w) "Hl2".
   clear Hlookup. assert (<[off:=w]> vs !! off = Some w) as Hlookup.
@@ -102,7 +102,7 @@ Proof.
 Qed.
 
 Lemma twp_allocN s E v n :
-  0 < n →
+  (0 < n)%Z →
   [[{ True }]] AllocN (Val $ LitV $ LitInt $ n) (Val v) @ s; E
   [[{ l, RET LitV (LitLoc l); l ↦∗ replicate (Z.to_nat n) v ∗
          [∗ list] i ∈ seq 0 (Z.to_nat n), meta_token (l +ₗ (i : nat)) ⊤ }]].
@@ -113,7 +113,7 @@ Proof.
   by iApply mapsto_seq_array.
 Qed.
 Lemma wp_allocN s E v n :
-  0 < n →
+  (0 < n)%Z →
   {{{ True }}} AllocN (Val $ LitV $ LitInt $ n) (Val v) @ s; E
   {{{ l, RET LitV (LitLoc l); l ↦∗ replicate (Z.to_nat n) v ∗
          [∗ list] i ∈ seq 0 (Z.to_nat n), meta_token (l +ₗ (i : nat)) ⊤ }}}.
@@ -123,7 +123,7 @@ Proof.
 Qed.
 
 Lemma twp_allocN_vec s E v n :
-  0 < n →
+  (0 < n)%Z →
   [[{ True }]]
     AllocN #n v @ s ; E
   [[{ l, RET #l; l ↦∗ vreplicate (Z.to_nat n) v ∗
@@ -133,7 +133,7 @@ Proof.
   iIntros (l) "[Hl Hm]". iApply "HΦ". rewrite vec_to_list_replicate. iFrame.
 Qed.
 Lemma wp_allocN_vec s E v n :
-  0 < n →
+  (0 < n)%Z →
   {{{ True }}}
     AllocN #n v @ s ; E
   {{{ l, RET #l; l ↦∗ vreplicate (Z.to_nat n) v ∗
diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index 4d821594cc685c12968115fc6ea32470ae6bdf48..52616a5aa8c706e47839f5511f054c7296b00dfb 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -64,7 +64,6 @@ Delimit Scope expr_scope with E.
 Delimit Scope val_scope with V.
 
 Module heap_lang.
-Open Scope Z_scope.
 
 (** Expressions and vals. *)
 Definition proph_id := positive.
@@ -526,7 +525,7 @@ Definition bin_op_eval_int (op : bin_op) (n1 n2 : Z) : option base_lit :=
   | LtOp => Some $ LitBool (bool_decide (n1 < n2))
   | EqOp => Some $ LitBool (bool_decide (n1 = n2))
   | OffsetOp => None (* Pointer arithmetic *)
-  end.
+  end%Z.
 
 Definition bin_op_eval_bool (op : bin_op) (b1 b2 : bool) : option base_lit :=
   match op with
@@ -580,14 +579,14 @@ Proof. by rewrite /heap_array right_id. Qed.
 
 Lemma heap_array_lookup l vs ow k :
   heap_array l vs !! k = Some ow ↔
-  ∃ j w, 0 ≤ j ∧ k = l +ₗ j ∧ ow = Some w ∧ vs !! (Z.to_nat j) = Some w.
+  ∃ j w, (0 ≤ j)%Z ∧ k = l +ₗ j ∧ ow = Some w ∧ vs !! (Z.to_nat j) = Some w.
 Proof.
   revert k l; induction vs as [|v' vs IH]=> l' l /=.
   { rewrite lookup_empty. naive_solver lia. }
   rewrite -insert_union_singleton_l lookup_insert_Some IH. split.
   - intros [[-> ?] | (Hl & j & w & ? & -> & -> & ?)].
     { eexists 0, _. rewrite loc_add_0. naive_solver lia. }
-    eexists (1 + j), _. rewrite loc_add_assoc !Z.add_1_l Z2Nat.inj_succ; auto with lia.
+    eexists (1 + j)%Z, _. rewrite loc_add_assoc !Z.add_1_l Z2Nat.inj_succ; auto with lia.
   - intros (j & w & ? & -> & -> & Hil). destruct (decide (j = 0)); simplify_eq/=.
     { rewrite loc_add_0; eauto. }
     right. split.
@@ -595,12 +594,12 @@ Proof.
     assert (Z.to_nat j = S (Z.to_nat (j - 1))) as Hj.
     { rewrite -Z2Nat.inj_succ; last lia. f_equal; lia. }
     rewrite Hj /= in Hil.
-    eexists (j - 1), _. rewrite loc_add_assoc Z.add_sub_assoc Z.add_simpl_l.
+    eexists (j - 1)%Z, _. rewrite loc_add_assoc Z.add_sub_assoc Z.add_simpl_l.
     auto with lia.
 Qed.
 
 Lemma heap_array_map_disjoint (h : gmap loc (option val)) (l : loc) (vs : list val) :
-  (∀ i, (0 ≤ i) → (i < length vs) → h !! (l +ₗ i) = None) →
+  (∀ i, (0 ≤ i)%Z → (i < length vs)%Z → h !! (l +ₗ i) = None) →
   (heap_array l vs) ##ₘ h.
 Proof.
   intros Hdisj. apply map_disjoint_spec=> l' v1 v2.
@@ -652,8 +651,8 @@ Inductive head_step : expr → state → list observation → expr → state →
   | ForkS e σ:
      head_step (Fork e) σ [] (Val $ LitV LitUnit) σ [e]
   | AllocNS n v σ l :
-     0 < n →
-     (∀ i, 0 ≤ i → i < n → σ.(heap) !! (l +ₗ i) = None) →
+     (0 < n)%Z →
+     (∀ i, (0 ≤ i)%Z → (i < n)%Z → σ.(heap) !! (l +ₗ i) = None) →
      head_step (AllocN (Val $ LitV $ LitInt n) (Val v)) σ
                []
                (Val $ LitV $ LitLoc l) (state_init_heap l n v σ)
@@ -721,7 +720,7 @@ Proof. revert Ki1. induction Ki2, Ki1; naive_solver eauto with f_equal. Qed.
 
 Lemma alloc_fresh v n σ :
   let l := fresh_locs (dom (gset loc) σ.(heap)) in
-  0 < n →
+  (0 < n)%Z →
   head_step (AllocN ((Val $ LitV $ LitInt $ n)) (Val v)) σ []
             (Val $ LitV $ LitLoc l) (state_init_heap l n v σ) [].
 Proof.
diff --git a/theories/heap_lang/lib/array.v b/theories/heap_lang/lib/array.v
index 0de0570c0dcc65dd1321bf018c1406c36e0df201..b41447205a3e874946ea48a82926baa566666eb0 100644
--- a/theories/heap_lang/lib/array.v
+++ b/theories/heap_lang/lib/array.v
@@ -81,7 +81,7 @@ Section proof.
 
   Theorem twp_array_clone stk E l q vl n :
     Z.of_nat (length vl) = n →
-    0 < n →
+    (0 < n)%Z →
     [[{ l ↦∗{q} vl }]]
       array_clone #l #n @ stk; E
     [[{ l', RET #l'; l' ↦∗ vl ∗ l ↦∗{q} vl }]].
@@ -98,7 +98,7 @@ Section proof.
   Qed.
   Theorem wp_array_clone stk E l q vl n :
     Z.of_nat (length vl) = n →
-    0 < n →
+    (0 < n)%Z →
     {{{ l ↦∗{q} vl }}}
       array_clone #l #n @ stk; E
     {{{ l', RET #l'; l' ↦∗ vl ∗ l ↦∗{q} vl }}}.
diff --git a/theories/heap_lang/lib/counter.v b/theories/heap_lang/lib/counter.v
index c7992d8b3ff5377d80f50d1004a9f3b9ecb94e76..52fc59ab725e7993111dc20c6525e41402d12a8e 100644
--- a/theories/heap_lang/lib/counter.v
+++ b/theories/heap_lang/lib/counter.v
@@ -39,7 +39,7 @@ Section mono_proof.
     iMod (own_alloc (● (O:mnat) ⋅ ◯ (O:mnat))) as (γ) "[Hγ Hγ']";
       first by apply auth_both_valid.
     iMod (inv_alloc N _ (mcounter_inv γ l) with "[Hl Hγ]").
-    { iNext. iExists 0%nat. by iFrame. }
+    { iNext. iExists 0. by iFrame. }
     iModIntro. iApply "HΦ". rewrite /mcounter; eauto 10.
   Qed.
 
@@ -70,7 +70,7 @@ Section mono_proof.
   Qed.
 
   Lemma read_mono_spec l j :
-    {{{ mcounter l j }}} read #l {{{ i, RET #i; ⌜j ≤ i⌝%nat ∧ mcounter l i }}}.
+    {{{ mcounter l j }}} read #l {{{ i, RET #i; ⌜j ≤ i⌝ ∧ mcounter l i }}}.
   Proof.
     iIntros (ϕ) "Hc HΦ". iDestruct "Hc" as (γ) "[#Hinv Hγf]".
     rewrite /read /=. wp_lam. iInv N as (c) ">[Hγ Hl]".
@@ -115,10 +115,10 @@ Section contrib_spec.
     {{{ γ l, RET #l; ccounter_ctx γ l ∗ ccounter γ 1 0 }}}.
   Proof.
     iIntros (Φ) "_ HΦ". rewrite -wp_fupd /newcounter /=. wp_lam. wp_alloc l as "Hl".
-    iMod (own_alloc (●F O%nat ⋅ ◯F 0%nat)) as (γ) "[Hγ Hγ']";
+    iMod (own_alloc (●F O ⋅ ◯F 0)) as (γ) "[Hγ Hγ']";
       first by apply auth_both_valid.
     iMod (inv_alloc N _ (ccounter_inv γ l) with "[Hl Hγ]").
-    { iNext. iExists 0%nat. by iFrame. }
+    { iNext. iExists 0. by iFrame. }
     iModIntro. iApply "HΦ". rewrite /ccounter_ctx /ccounter; eauto 10.
   Qed.
 
@@ -144,7 +144,7 @@ Section contrib_spec.
 
   Lemma read_contrib_spec γ l q n :
     {{{ ccounter_ctx γ l ∗ ccounter γ q n }}} read #l
-    {{{ c, RET #c; ⌜n ≤ c⌝%nat ∧ ccounter γ q n }}}.
+    {{{ c, RET #c; ⌜n ≤ c⌝ ∧ ccounter γ q n }}}.
   Proof.
     iIntros (Φ) "[#? Hγf] HΦ".
     rewrite /read /=. wp_lam. iInv N as (c) ">[Hγ Hl]". wp_load.
diff --git a/theories/heap_lang/lib/ticket_lock.v b/theories/heap_lang/lib/ticket_lock.v
index 82ce5f2f921c44cf9ee00b2b6f87ec1b0454a051..311c7ae2146c0350cd18c3591860aa65a90d7424 100644
--- a/theories/heap_lang/lib/ticket_lock.v
+++ b/theories/heap_lang/lib/ticket_lock.v
@@ -85,11 +85,11 @@ Section proof.
   Proof.
     iIntros (Φ) "HR HΦ". rewrite -wp_fupd. wp_lam.
     wp_alloc ln as "Hln". wp_alloc lo as "Hlo".
-    iMod (own_alloc (● (Excl' 0%nat, GSet ∅) ⋅ ◯ (Excl' 0%nat, GSet ∅))) as (γ) "[Hγ Hγ']".
+    iMod (own_alloc (● (Excl' 0, GSet ∅) ⋅ ◯ (Excl' 0, GSet ∅))) as (γ) "[Hγ Hγ']".
     { by apply auth_both_valid. }
     iMod (inv_alloc _ _ (lock_inv γ lo ln R) with "[-HΦ]").
     { iNext. rewrite /lock_inv.
-      iExists 0%nat, 0%nat. iFrame. iLeft. by iFrame. }
+      iExists 0, 0. iFrame. iLeft. by iFrame. }
     wp_pures. iModIntro. iApply ("HΦ" $! (#lo, #ln)%V γ). iExists lo, ln. eauto.
   Qed.
 
diff --git a/theories/heap_lang/metatheory.v b/theories/heap_lang/metatheory.v
index 0859f72697bf77ceb005cfa330cc3431dc39d39a..5ff1dcb674762b21046e552d9d0d8bdd819a9056 100644
--- a/theories/heap_lang/metatheory.v
+++ b/theories/heap_lang/metatheory.v
@@ -93,10 +93,10 @@ Proof.
 Qed.
 
 Lemma heap_closed_alloc σ l n w :
-  0 < n →
+  (0 < n)%Z →
   is_closed_val w →
   map_Forall (λ _ v, from_option is_closed_val true v) (heap σ) →
-  (∀ i : Z, 0 ≤ i → i < n → heap σ !! (l +ₗ i) = None) →
+  (∀ i : Z, (0 ≤ i)%Z → (i < n)%Z → heap σ !! (l +ₗ i) = None) →
   map_Forall (λ _ v, from_option is_closed_val true v)
              (heap_array l (replicate (Z.to_nat n) w) ∪ heap σ).
 Proof.
diff --git a/theories/heap_lang/primitive_laws.v b/theories/heap_lang/primitive_laws.v
index 9f004324fdd8655f881bca54cd5a42fb60ab6231..ecc290cff8b287d7b8bc521513b8a04af9d40140 100644
--- a/theories/heap_lang/primitive_laws.v
+++ b/theories/heap_lang/primitive_laws.v
@@ -397,7 +397,7 @@ Proof.
 Qed.
 
 Lemma twp_allocN_seq s E v n :
-  0 < n →
+  (0 < n)%Z →
   [[{ True }]] AllocN (Val $ LitV $ LitInt $ n) (Val v) @ s; E
   [[{ l, RET LitV (LitLoc l); [∗ list] i ∈ seq 0 (Z.to_nat n),
       (l +ₗ (i : nat)) ↦ v ∗ meta_token (l +ₗ (i : nat)) ⊤ }]].
@@ -415,7 +415,7 @@ Proof.
   - iApply (heap_array_to_seq_meta with "Hm"). by rewrite replicate_length.
 Qed.
 Lemma wp_allocN_seq s E v n :
-  0 < n →
+  (0 < n)%Z →
   {{{ True }}} AllocN (Val $ LitV $ LitInt $ n) (Val v) @ s; E
   {{{ l, RET LitV (LitLoc l); [∗ list] i ∈ seq 0 (Z.to_nat n),
       (l +ₗ (i : nat)) ↦ v ∗ meta_token (l +ₗ (i : nat)) ⊤ }}}.
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index 28eae1b6f4be01417d72bd52229a1d7d5a87798e..739d78cea7864d2d1c15564a87d838fd190678b9 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -183,7 +183,7 @@ Implicit Types v : val.
 Implicit Types z : Z.
 
 Lemma tac_wp_allocN Δ Δ' s E j K v n Φ :
-  0 < n →
+  (0 < n)%Z →
   MaybeIntoLaterNEnvs 1 Δ Δ' →
   (∀ l, ∃ Δ'',
     envs_app false (Esnoc Enil j (array l 1 (replicate (Z.to_nat n) v))) Δ' = Some Δ'' ∧
@@ -197,7 +197,7 @@ Proof.
   apply wand_intro_l. by rewrite (sep_elim_l (l ↦∗ _)%I) right_id wand_elim_r.
 Qed.
 Lemma tac_twp_allocN Δ s E j K v n Φ :
-  0 < n →
+  (0 < n)%Z →
   (∀ l, ∃ Δ',
     envs_app false (Esnoc Enil j (array l 1 (replicate (Z.to_nat n) v))) Δ
     = Some Δ' ∧
@@ -407,7 +407,7 @@ Qed.
 Lemma tac_wp_faa Δ Δ' Δ'' s E i K l z1 z2 Φ :
   MaybeIntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦ LitV z1)%I →
-  envs_simple_replace i false (Esnoc Enil i (l ↦ LitV (z1 + z2))) Δ' = Some Δ'' →
+  envs_simple_replace i false (Esnoc Enil i (l ↦ LitV (LitInt (z1 + z2)))) Δ' = Some Δ'' →
   envs_entails Δ'' (WP fill K (Val $ LitV z1) @ s; E {{ Φ }}) →
   envs_entails Δ (WP fill K (FAA (LitV l) (LitV z2)) @ s; E {{ Φ }}).
 Proof.
@@ -418,7 +418,7 @@ Proof.
 Qed.
 Lemma tac_twp_faa Δ Δ' s E i K l z1 z2 Φ :
   envs_lookup i Δ = Some (false, l ↦ LitV z1)%I →
-  envs_simple_replace i false (Esnoc Enil i (l ↦ LitV (z1 + z2))) Δ = Some Δ' →
+  envs_simple_replace i false (Esnoc Enil i (l ↦ LitV (LitInt (z1 + z2)))) Δ = Some Δ' →
   envs_entails Δ' (WP fill K (Val $ LitV z1) @ s; E [{ Φ }]) →
   envs_entails Δ (WP fill K (FAA (LitV l) (LitV z2)) @ s; E [{ Φ }]).
 Proof.
diff --git a/theories/heap_lang/proph_erasure.v b/theories/heap_lang/proph_erasure.v
index ca5671830b9c4ee7e80cfa383c4266d50a99de73..a568a68c3d439311fe78f73f39647cf508102985 100644
--- a/theories/heap_lang/proph_erasure.v
+++ b/theories/heap_lang/proph_erasure.v
@@ -245,8 +245,8 @@ Lemma erased_head_step_head_step_NewProph σ :
   head_steps_to_erasure_of NewProph σ #LitPoison (erase_state σ) [].
 Proof. eexists _, _, _, _; split; first eapply new_proph_id_fresh; done. Qed.
 Lemma erased_head_step_head_step_AllocN n v σ l :
-  0 < n →
-  (∀ i : Z, 0 ≤ i → i < n → erase_heap (heap σ) !! (l +ₗ i) = None) →
+  (0 < n)%Z →
+  (∀ i : Z, (0 ≤ i)%Z → (i < n)%Z → erase_heap (heap σ) !! (l +ₗ i) = None) →
   head_steps_to_erasure_of
     (AllocN #n v) σ #l (state_init_heap l n (erase_val v) (erase_state σ)) [].
 Proof.
@@ -508,9 +508,8 @@ Proof.
   (** Case split on whether e1 is a [Resolve] expression. *)
   destruct (decide (is_Resolve e1)); last first.
   { (** e1 is not a [Resolve] expression. *)
-    eapply non_resolve_prim_step_matched_by_erased_steps_ectx_item; eauto; [|].
-    - by eapply fill_not_val, val_head_stuck.
-    - intros; eapply (IH K); simpl; eauto with lia. }
+    eapply non_resolve_prim_step_matched_by_erased_steps_ectx_item; [|by eauto..].
+    by eapply fill_not_val, val_head_stuck. }
   (** e1 is a [Resolve] expression. *)
   destruct Ki; simplify_eq/=;
     repeat
@@ -677,7 +676,8 @@ Proof.
 Qed.
 
 Lemma head_step_erased_prim_step_allocN σ l n v:
-  0 < n → (∀ i : Z, 0 ≤ i → i < n → heap σ !! (l +ₗ i) = None) →
+  (0 < n)%Z →
+  (∀ i : Z, (0 ≤ i)%Z → (i < n)%Z → heap σ !! (l +ₗ i) = None) →
   ∃ e2' σ2' ef',
     prim_step (AllocN #n (erase_val v)) (erase_state σ) [] e2' σ2' ef'.
 Proof.