diff --git a/CHANGELOG.md b/CHANGELOG.md
index efb51c925ff73267f87c2d6d7656f55ab2ba0318..3330e7f258f51bc7d896b2536e59d406d42e79d9 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -63,6 +63,10 @@ Coq 8.13 is no longer supported.
 * Add `IsExcept0` instance for invariants, allowing you to remove laters of
   timeless hypotheses when proving an invariant (without an update).
 
+**Changes in `heap_lang`:**
+
+* Move operations and lemmas about locations into a module `Loc`.
+
 **LaTeX changes:**
 
 - Rename `\Alloc` to `\AllocN` and `\Ref` to `\Alloc` for better consistency
@@ -78,6 +82,9 @@ s/iSolveTC\b/tc_solve/g
 # _alt -> _def
 s/\bsig_equiv_alt\b/sig_equiv_def/g
 s/\bsig_dist_alt\b/sig_dist_def/g
+# Loc
+s/\bloc_add(_assoc|_0|_inj|)\b/Loc.add\1/g
+s/\bfresh_locs(_fresh|)\b/Loc.fresh\1/g
 EOF
 ```
 
diff --git a/iris_heap_lang/derived_laws.v b/iris_heap_lang/derived_laws.v
index 2f8cba8db7d4e54436899544a5b54d208c1983f2..71858a63ac9831705505f483bf593aceaf9d2a40 100644
--- a/iris_heap_lang/derived_laws.v
+++ b/iris_heap_lang/derived_laws.v
@@ -45,20 +45,20 @@ Lemma array_nil l dq : l ↦∗{dq} [] ⊣⊢ emp.
 Proof. by rewrite /array. Qed.
 
 Lemma array_singleton l dq v : l ↦∗{dq} [v] ⊣⊢ l ↦{dq} v.
-Proof. by rewrite /array /= right_id loc_add_0. Qed.
+Proof. by rewrite /array /= right_id Loc.add_0. Qed.
 
 Lemma array_app l dq vs ws :
   l ↦∗{dq} (vs ++ ws) ⊣⊢ l ↦∗{dq} vs ∗ (l +ₗ length vs) ↦∗{dq} ws.
 Proof.
   rewrite /array big_sepL_app.
   setoid_rewrite Nat2Z.inj_add.
-  by setoid_rewrite loc_add_assoc.
+  by setoid_rewrite Loc.add_assoc.
 Qed.
 
 Lemma array_cons l dq v vs : l ↦∗{dq} (v :: vs) ⊣⊢ l ↦{dq} v ∗ (l +ₗ 1) ↦∗{dq} vs.
 Proof.
-  rewrite /array big_sepL_cons loc_add_0.
-  setoid_rewrite loc_add_assoc.
+  rewrite /array big_sepL_cons Loc.add_0.
+  setoid_rewrite Loc.add_assoc.
   setoid_rewrite Nat2Z.inj_succ.
   by setoid_rewrite Z.add_1_l.
 Qed.
@@ -96,7 +96,7 @@ Proof.
   { done. }
   iIntros "[$ Hl]". rewrite -fmap_S_seq big_sepL_fmap.
   setoid_rewrite Nat2Z.inj_succ. setoid_rewrite <-Z.add_1_l.
-  setoid_rewrite <-loc_add_assoc. iApply "IH". done.
+  setoid_rewrite <-Loc.add_assoc. iApply "IH". done.
 Qed.
 
 Lemma twp_allocN s E v n :
diff --git a/iris_heap_lang/lang.v b/iris_heap_lang/lang.v
index 4141e9e45fc2a8599ee3ee08259b6c208c313674..f75cdc21161ff46c8cab2778a811a0efdef641df 100644
--- a/iris_heap_lang/lang.v
+++ b/iris_heap_lang/lang.v
@@ -603,16 +603,16 @@ Proof.
   { 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)%Z, _. rewrite loc_add_assoc !Z.add_1_l Z2Nat.inj_succ; auto with lia.
+    { eexists 0, _. rewrite Loc.add_0. naive_solver 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. }
+    { rewrite Loc.add_0; eauto. }
     right. split.
-    { rewrite -{1}(loc_add_0 l). intros ?%(inj (loc_add _)); lia. }
+    { rewrite -{1}(Loc.add_0 l). intros ?%(inj (Loc.add _)); lia. }
     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)%Z, _. 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.
 
@@ -746,7 +746,7 @@ Proof.
 Qed.
 
 Lemma alloc_fresh v n σ :
-  let l := fresh_locs (dom σ.(heap)) in
+  let l := Loc.fresh (dom σ.(heap)) in
   (0 < n)%Z →
   head_step (AllocN ((Val $ LitV $ LitInt $ n)) (Val v)) σ []
             (Val $ LitV $ LitLoc l) (state_init_heap l n v σ) [].
@@ -754,7 +754,7 @@ Proof.
   intros.
   apply AllocNS; first done.
   intros. apply not_elem_of_dom.
-  by apply fresh_locs_fresh.
+  by apply Loc.fresh_fresh.
 Qed.
 
 Lemma new_proph_id_fresh σ :
diff --git a/iris_heap_lang/lib/array.v b/iris_heap_lang/lib/array.v
index 15f88e961ac3117d4880c0a6b39184e7dac651c9..a55c84bb2155cba6926b332d1339e575091683a6 100644
--- a/iris_heap_lang/lib/array.v
+++ b/iris_heap_lang/lib/array.v
@@ -150,10 +150,10 @@ Section proof.
       wp_smart_apply (wp_wand with "Hf"); iIntros (v) "Hv". wp_store. wp_pures.
       rewrite Z.add_1_r -Nat2Z.inj_succ.
       iApply ("IH" with "[%] [HSl] HSf"); first lia.
-      { by rewrite loc_add_assoc Z.add_1_r -Nat2Z.inj_succ. }
+      { by rewrite Loc.add_assoc Z.add_1_r -Nat2Z.inj_succ. }
       iIntros "!>" (vs). iDestruct 1 as (<-) "[HSl Hvs]".
       iApply ("HΦ" $! (v :: vs)). iSplit; [naive_solver|]. iSplitL "Hl HSl".
-      - iFrame "Hl". by rewrite loc_add_assoc Z.add_1_r -Nat2Z.inj_succ.
+      - iFrame "Hl". by rewrite Loc.add_assoc Z.add_1_r -Nat2Z.inj_succ.
       - iEval (rewrite /= Nat.add_0_r; setoid_rewrite Nat.add_succ_r). iFrame.
     Qed.
     Local Lemma twp_array_init_loop stk E l i n k f  :
@@ -177,10 +177,10 @@ Section proof.
       wp_smart_apply (twp_wand with "Hf"); iIntros (v) "Hv". wp_store. wp_pures.
       rewrite Z.add_1_r -Nat2Z.inj_succ.
       iApply ("IH" with "[%] [HSl] HSf"); first lia.
-      { by rewrite loc_add_assoc Z.add_1_r -Nat2Z.inj_succ. }
+      { by rewrite Loc.add_assoc Z.add_1_r -Nat2Z.inj_succ. }
       iIntros (vs). iDestruct 1 as (<-) "[HSl Hvs]".
       iApply ("HΦ" $! (v :: vs)). iSplit; [naive_solver|]. iSplitL "Hl HSl".
-      - iFrame "Hl". by rewrite loc_add_assoc Z.add_1_r -Nat2Z.inj_succ.
+      - iFrame "Hl". by rewrite Loc.add_assoc Z.add_1_r -Nat2Z.inj_succ.
       - iEval (rewrite /= Nat.add_0_r; setoid_rewrite Nat.add_succ_r). iFrame.
     Qed.
 
@@ -197,11 +197,11 @@ Section proof.
       iIntros (Hn Φ) "Hf HΦ". wp_lam. wp_alloc l as "Hl"; first done.
       wp_smart_apply (wp_array_init_loop _ _ _ 0 n (Z.to_nat n) with "[Hl $Hf] [HΦ]").
       { by rewrite /= Z2Nat.id; last lia. }
-      { by rewrite loc_add_0. }
+      { by rewrite Loc.add_0. }
       iIntros "!>" (vs). iDestruct 1 as (Hlen) "[Hl Hvs]". wp_pures.
       iApply ("HΦ" $! _ vs). iModIntro. iSplit.
       { iPureIntro. by rewrite Hlen Z2Nat.id; last lia. }
-      rewrite loc_add_0. iFrame.
+      rewrite Loc.add_0. iFrame.
     Qed.
     Lemma twp_array_init stk E n f :
       (0 < n)%Z →
@@ -216,11 +216,11 @@ Section proof.
       iIntros (Hn Φ) "Hf HΦ". wp_lam. wp_alloc l as "Hl"; first done.
       wp_smart_apply (twp_array_init_loop _ _ _ 0 n (Z.to_nat n) with "[Hl $Hf] [HΦ]").
       { by rewrite /= Z2Nat.id; last lia. }
-      { by rewrite loc_add_0. }
+      { by rewrite Loc.add_0. }
       iIntros (vs). iDestruct 1 as (Hlen) "[Hl Hvs]". wp_pures.
       iApply ("HΦ" $! _ vs). iModIntro. iSplit.
       { iPureIntro. by rewrite Hlen Z2Nat.id; last lia. }
-      rewrite loc_add_0. iFrame.
+      rewrite Loc.add_0. iFrame.
     Qed.
   End array_init.
 
diff --git a/iris_heap_lang/locations.v b/iris_heap_lang/locations.v
index a11775e143c23b4ad3150e8c3699f67c1893bb8e..ac67d09f126951794282d3ec639ebf015bd4d69f 100644
--- a/iris_heap_lang/locations.v
+++ b/iris_heap_lang/locations.v
@@ -6,43 +6,54 @@ Record loc := Loc { loc_car : Z }.
 
 Add Printing Constructor loc.
 
-Global Instance loc_eq_decision : EqDecision loc.
-Proof. solve_decision. Defined.
+Module Loc.
+  Local Open Scope Z_scope.
 
-Global Instance loc_inhabited : Inhabited loc := populate {|loc_car := 0 |}.
+  Lemma eq_spec l1 l2 : l1 = l2 ↔ loc_car l1 = loc_car l2.
+  Proof. destruct l1, l2; naive_solver. Qed.
 
-Global Instance loc_countable : Countable loc.
-Proof. by apply (inj_countable' loc_car Loc); intros []. Defined.
+  Global Instance eq_dec : EqDecision loc.
+  Proof. solve_decision. Defined.
 
-Global Program Instance loc_infinite : Infinite loc :=
-  inj_infinite (λ p, {| loc_car := p |}) (λ l, Some (loc_car l)) _.
-Next Obligation. done. Qed.
+  Global Instance inhabited : Inhabited loc := populate {|loc_car := 0 |}.
 
-Definition loc_add (l : loc) (off : Z) : loc :=
-  {| loc_car := loc_car l + off|}.
+  Global Instance countable : Countable loc.
+  Proof. by apply (inj_countable' loc_car Loc); intros []. Defined.
 
-Notation "l +â‚— off" :=
-  (loc_add l off) (at level 50, left associativity) : stdpp_scope.
+  Global Program Instance infinite : Infinite loc :=
+    inj_infinite (λ p, {| loc_car := p |}) (λ l, Some (loc_car l)) _.
+  Next Obligation. done. Qed.
 
-Lemma loc_add_assoc l i j : l +â‚— i +â‚— j = l +â‚— (i + j).
-Proof. destruct l; rewrite /loc_add /=; f_equal; lia. Qed.
+  Definition add (l : loc) (off : Z) : loc :=
+    {| loc_car := loc_car l + off|}.
 
-Lemma loc_add_0 l : l +â‚— 0 = l.
-Proof. destruct l; rewrite /loc_add /=; f_equal; lia. Qed.
+  Module Import notations.
+    Notation "l +â‚— off" :=
+      (add l off) (at level 50, left associativity) : stdpp_scope.
+  End notations.
 
-Global Instance loc_add_inj l : Inj eq eq (loc_add l).
-Proof. destruct l; rewrite /Inj /loc_add /=; intros; simplify_eq; lia. Qed.
+  Lemma add_assoc l i j : l +â‚— i +â‚— j = l +â‚— (i + j).
+  Proof. rewrite eq_spec /=. lia. Qed.
 
-Definition fresh_locs (ls : gset loc) : loc :=
-  {| loc_car := set_fold (λ k r, (1 + loc_car k) `max` r)%Z 1%Z ls |}.
+  Lemma add_0 l : l +â‚— 0 = l.
+  Proof. rewrite eq_spec /=; lia. Qed.
 
-Lemma fresh_locs_fresh ls i :
-  (0 ≤ i)%Z → fresh_locs ls +ₗ i ∉ ls.
-Proof.
-  intros Hi. cut (∀ l, l ∈ ls → loc_car l < loc_car (fresh_locs ls) + i)%Z.
-  { intros help Hf%help. simpl in *. lia. }
-  apply (set_fold_ind_L (λ r ls, ∀ l, l ∈ ls → (loc_car l < r + i)%Z));
-    set_solver by eauto with lia.
-Qed.
+  Global Instance add_inj l : Inj eq eq (add l).
+  Proof. intros x1 x2. rewrite eq_spec /=. lia. Qed.
 
-Global Opaque fresh_locs.
+  Definition fresh (ls : gset loc) : loc :=
+    {| loc_car := set_fold (λ k r, (1 + loc_car k) `max` r) 1 ls |}.
+
+  Lemma fresh_fresh ls i :
+    (0 ≤ i)%Z → fresh ls +ₗ i ∉ ls.
+  Proof.
+    intros Hi. cut (∀ l, l ∈ ls → loc_car l < loc_car (fresh ls) + i).
+    { intros help Hf%help. simpl in *. lia. }
+    apply (set_fold_ind_L (λ r ls, ∀ l, l ∈ ls → (loc_car l < r + i)));
+      set_solver by eauto with lia.
+  Qed.
+
+  Global Opaque fresh.
+End Loc.
+
+Export Loc.notations.
diff --git a/iris_heap_lang/primitive_laws.v b/iris_heap_lang/primitive_laws.v
index 6d5326c552f2fbc62419c02aace1f65eaba22ee5..050b62ce661e870b28b1af9c4ac7e1b62fe7c1c4 100644
--- a/iris_heap_lang/primitive_laws.v
+++ b/iris_heap_lang/primitive_laws.v
@@ -298,10 +298,10 @@ Proof.
   rewrite big_opM_union; last first.
   { apply map_disjoint_spec=> l' v1 v2 /lookup_singleton_Some [-> _].
     intros (j&w&?&Hjl&?&?)%heap_array_lookup.
-    rewrite loc_add_assoc -{1}[l']loc_add_0 in Hjl. simplify_eq; lia. }
-  rewrite loc_add_0 -fmap_S_seq big_sepL_fmap.
+    rewrite Loc.add_assoc -{1}[l']Loc.add_0 in Hjl. simplify_eq; lia. }
+  rewrite Loc.add_0 -fmap_S_seq big_sepL_fmap.
   setoid_rewrite Nat2Z.inj_succ. setoid_rewrite <-Z.add_1_l.
-  setoid_rewrite <-loc_add_assoc.
+  setoid_rewrite <-Loc.add_assoc.
   rewrite big_opM_singleton; iDestruct "Hvs" as "[$ Hvs]". by iApply "IH".
 Qed.
 
@@ -314,10 +314,10 @@ Proof.
   rewrite big_opM_union; last first.
   { apply map_disjoint_spec=> l' v1 v2 /lookup_singleton_Some [-> _].
     intros (j&w&?&Hjl&_)%heap_array_lookup.
-    rewrite loc_add_assoc -{1}[l']loc_add_0 in Hjl. simplify_eq; lia. }
-  rewrite loc_add_0 -fmap_S_seq big_sepL_fmap.
+    rewrite Loc.add_assoc -{1}[l']Loc.add_0 in Hjl. simplify_eq; lia. }
+  rewrite Loc.add_0 -fmap_S_seq big_sepL_fmap.
   setoid_rewrite Nat2Z.inj_succ. setoid_rewrite <-Z.add_1_l.
-  setoid_rewrite <-loc_add_assoc.
+  setoid_rewrite <-Loc.add_assoc.
   rewrite big_opM_singleton; iDestruct "Hvs" as "[$ Hvs]". by iApply "IH".
 Qed.
 
@@ -354,7 +354,7 @@ Lemma twp_alloc s E v :
   [[{ True }]] Alloc (Val v) @ s; E [[{ l, RET LitV (LitLoc l); l ↦ v ∗ meta_token l ⊤ }]].
 Proof.
   iIntros (Φ) "_ HΦ". iApply twp_allocN_seq; [auto with lia..|].
-  iIntros (l) "/= (? & _)". rewrite loc_add_0. iApply "HΦ"; iFrame.
+  iIntros (l) "/= (? & _)". rewrite Loc.add_0. iApply "HΦ"; iFrame.
 Qed.
 Lemma wp_alloc s E v :
   {{{ True }}} Alloc (Val v) @ s; E {{{ l, RET LitV (LitLoc l); l ↦ v ∗ meta_token l ⊤ }}}.