diff --git a/CHANGELOG.md b/CHANGELOG.md
index 3d307cbe24bf664e8146e82b6c59c24d1b13e4a8..b1c497ad9074d7af96463077776dc7eef00577ac 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -196,6 +196,8 @@ Coq development, but not every API-breaking change is listed.  Changes marked
 * Rename `inv_sep_1` → `inv_split_1`, `inv_sep_2` → `inv_split_2`, and
   `inv_sep` → `inv_split` to be consistent with the naming convention in boxes.
 * 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`.
 
 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/_CoqProject b/_CoqProject
index aa95ee16316aa7da30fe22d61a7809e17239e31b..036d7ec249862df678cbeaa8a437ef7a626b7689 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -104,8 +104,8 @@ theories/heap_lang/locations.v
 theories/heap_lang/lang.v
 theories/heap_lang/metatheory.v
 theories/heap_lang/tactics.v
-theories/heap_lang/lifting.v
-theories/heap_lang/array.v
+theories/heap_lang/primitive_laws.v
+theories/heap_lang/derived_laws.v
 theories/heap_lang/notation.v
 theories/heap_lang/proofmode.v
 theories/heap_lang/adequacy.v
diff --git a/tests/atomic.v b/tests/atomic.v
index 7e9ed07265975eb58bfd67a8f102d1c330600478..f9881ffcd85934e945e3837e5a13bf60770d41a2 100644
--- a/tests/atomic.v
+++ b/tests/atomic.v
@@ -1,6 +1,5 @@
 From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export atomic.
-From iris.heap_lang Require Export lifting notation.
 From iris.heap_lang Require Import proofmode notation atomic_heap.
 Set Default Proof Using "Type".
 
diff --git a/tests/heap_lang2.v b/tests/heap_lang2.v
index 85dcae1bcf41917c66aa260815df078b66cb9a30..4ec6061ccf3f41787e5b1c017043c424d7d7d00f 100644
--- a/tests/heap_lang2.v
+++ b/tests/heap_lang2.v
@@ -1,7 +1,7 @@
 (* Test yet another way of importing heap_lang modules that used to break
 printing *)
 From iris.proofmode Require Import tactics.
-From iris.heap_lang Require Export lifting notation.
+From iris.heap_lang Require Export primitive_laws notation.
 From iris.heap_lang Require Import proofmode notation.
 Set Default Proof Using "Type".
 
diff --git a/theories/heap_lang/array.v b/theories/heap_lang/derived_laws.v
similarity index 85%
rename from theories/heap_lang/array.v
rename to theories/heap_lang/derived_laws.v
index 43879b05b8b575f9d54e1e2ad5dbf93fa398dee5..1e36d1f7a9df0788677250eb80a308613c1bd529 100644
--- a/theories/heap_lang/array.v
+++ b/theories/heap_lang/derived_laws.v
@@ -1,13 +1,18 @@
+(** This file extends the HeapLang program logic with some derived laws (not
+using the lifting lemmas) about arrays and prophecies.
+
+For utility functions on arrays (e.g., freeing/copying an array), see
+[heap_lang.lib.array].  *)
+
 From stdpp Require Import fin_maps.
 From iris.bi Require Import lib.fractional.
 From iris.proofmode Require Import tactics.
-From iris.heap_lang Require Export lifting.
+From iris.heap_lang Require Export primitive_laws.
 From iris.heap_lang Require Import tactics notation.
 Set Default Proof Using "Type".
 
-(** This file defines the [array] connective, a version of [mapsto] that works
-with lists of values. It also contains array versions of the basic heap
-operations of HeapLang. *)
+(** The [array] connective is a version of [mapsto] that works
+with lists of values. *)
 
 Definition array `{!heapG Σ} (l : loc) (q : Qp) (vs : list val) : iProp Σ :=
   ([∗ list] i ↦ v ∈ vs, (l +ₗ i) ↦{q} v)%I.
@@ -317,6 +322,45 @@ Proof.
   iIntros (? Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
   iApply (twp_faa_offset_vec with "H"); [eauto..|]; iIntros "H HΦ". by iApply "HΦ".
 Qed.
+
+(** Derived prophecy laws *)
+
+(** Lemmas for some particular expression inside the [Resolve]. *)
+Lemma wp_resolve_proph s E (p : proph_id) (pvs : list (val * val)) v :
+  {{{ proph p pvs }}}
+    ResolveProph (Val $ LitV $ LitProphecy p) (Val v) @ s; E
+  {{{ pvs', RET (LitV LitUnit); ⌜pvs = (LitV LitUnit, v)::pvs'⌝ ∗ proph p pvs' }}}.
+Proof.
+  iIntros (Φ) "Hp HΦ". iApply (wp_resolve with "Hp"); first done.
+  iApply lifting.wp_pure_step_later=> //=. iApply wp_value.
+  iIntros "!>" (vs') "HEq Hp". iApply "HΦ". iFrame.
+Qed.
+
+Lemma wp_resolve_cmpxchg_suc s E l (p : proph_id) (pvs : list (val * val)) v1 v2 v :
+  vals_compare_safe v1 v1 →
+  {{{ proph p pvs ∗ ▷ l ↦ v1 }}}
+    Resolve (CmpXchg #l v1 v2) #p v @ s; E
+  {{{ RET (v1, #true) ; ∃ pvs', ⌜pvs = ((v1, #true)%V, v)::pvs'⌝ ∗ proph p pvs' ∗ l ↦ v2 }}}.
+Proof.
+  iIntros (Hcmp Φ) "[Hp Hl] HΦ".
+  iApply (wp_resolve with "Hp"); first done.
+  assert (val_is_unboxed v1) as Hv1; first by destruct Hcmp.
+  iApply (wp_cmpxchg_suc with "Hl"); [done..|]. iIntros "!> Hl".
+  iIntros (pvs' ->) "Hp". iApply "HΦ". eauto with iFrame.
+Qed.
+
+Lemma wp_resolve_cmpxchg_fail s E l (p : proph_id) (pvs : list (val * val)) q v' v1 v2 v :
+  v' ≠ v1 → vals_compare_safe v' v1 →
+  {{{ proph p pvs ∗ ▷ l ↦{q} v' }}}
+    Resolve (CmpXchg #l v1 v2) #p v @ s; E
+  {{{ RET (v', #false) ; ∃ pvs', ⌜pvs = ((v', #false)%V, v)::pvs'⌝ ∗ proph p pvs' ∗ l ↦{q} v' }}}.
+Proof.
+  iIntros (NEq Hcmp Φ) "[Hp Hl] HΦ".
+  iApply (wp_resolve with "Hp"); first done.
+  iApply (wp_cmpxchg_fail with "Hl"); [done..|]. iIntros "!> Hl".
+  iIntros (pvs' ->) "Hp". iApply "HΦ". eauto with iFrame.
+Qed.
+
 End lifting.
 
 Typeclasses Opaque array.
diff --git a/theories/heap_lang/lib/array.v b/theories/heap_lang/lib/array.v
index 364c806d40ebfd99d70afc81161e86847a6f7332..0de0570c0dcc65dd1321bf018c1406c36e0df201 100644
--- a/theories/heap_lang/lib/array.v
+++ b/theories/heap_lang/lib/array.v
@@ -1,6 +1,6 @@
 From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export weakestpre.
-From iris.heap_lang Require Export lang array.
+From iris.heap_lang Require Export derived_laws.
 From iris.heap_lang Require Import proofmode notation.
 Set Default Proof Using "Type".
 
diff --git a/theories/heap_lang/lib/atomic_heap.v b/theories/heap_lang/lib/atomic_heap.v
index 6a762620f87bea32bbe36bda152b90e8911d6cd0..bdbc3783861f96a61fd7f797d258353b2b81ecaf 100644
--- a/theories/heap_lang/lib/atomic_heap.v
+++ b/theories/heap_lang/lib/atomic_heap.v
@@ -1,8 +1,8 @@
 From iris.bi.lib Require Import fractional.
 From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export atomic.
-From iris.heap_lang Require Export lifting notation.
-From iris.heap_lang Require Import proofmode.
+From iris.heap_lang Require Export derived_laws.
+From iris.heap_lang Require Import notation proofmode.
 Set Default Proof Using "Type".
 
 (** A general logically atomic interface for a heap. *)
@@ -149,4 +149,4 @@ Definition primitive_atomic_heap `{!heapG Σ} : atomic_heap Σ :=
      load_spec := primitive_load_spec;
      store_spec := primitive_store_spec;
      cmpxchg_spec := primitive_cmpxchg_spec;
-     mapsto_agree := lifting.mapsto_agree |}.
+     mapsto_agree := primitive_laws.mapsto_agree |}.
diff --git a/theories/heap_lang/lib/lock.v b/theories/heap_lang/lib/lock.v
index 77f57e59b7a2dd437c9dabbeec77213750ad8cbb..0430aec748b016e6935baee9c52802fa5b03b639 100644
--- a/theories/heap_lang/lib/lock.v
+++ b/theories/heap_lang/lib/lock.v
@@ -1,5 +1,5 @@
 From iris.base_logic.lib Require Export invariants.
-From iris.heap_lang Require Export lifting notation.
+From iris.heap_lang Require Import primitive_laws notation.
 Set Default Proof Using "Type".
 
 Structure lock Σ `{!heapG Σ} := Lock {
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/primitive_laws.v
similarity index 94%
rename from theories/heap_lang/lifting.v
rename to theories/heap_lang/primitive_laws.v
index c671e36a263c0d81e4587f477155fcae4dd57ea4..9f004324fdd8655f881bca54cd5a42fb60ab6231 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/primitive_laws.v
@@ -1,3 +1,6 @@
+(** This file proves the basic laws of the HeapLang program logic by applying
+the Iris lifting lemmas. *)
+
 From stdpp Require Import fin_maps.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth gmap.
@@ -623,40 +626,4 @@ Proof.
     iMod "HΦ". iModIntro. by iApply "HΦ".
 Qed.
 
-(** Lemmas for some particular expression inside the [Resolve]. *)
-Lemma wp_resolve_proph s E (p : proph_id) (pvs : list (val * val)) v :
-  {{{ proph p pvs }}}
-    ResolveProph (Val $ LitV $ LitProphecy p) (Val v) @ s; E
-  {{{ pvs', RET (LitV LitUnit); ⌜pvs = (LitV LitUnit, v)::pvs'⌝ ∗ proph p pvs' }}}.
-Proof.
-  iIntros (Φ) "Hp HΦ". iApply (wp_resolve with "Hp"); first done.
-  iApply wp_pure_step_later=> //=. iApply wp_value.
-  iIntros "!>" (vs') "HEq Hp". iApply "HΦ". iFrame.
-Qed.
-
-Lemma wp_resolve_cmpxchg_suc s E l (p : proph_id) (pvs : list (val * val)) v1 v2 v :
-  vals_compare_safe v1 v1 →
-  {{{ proph p pvs ∗ ▷ l ↦ v1 }}}
-    Resolve (CmpXchg #l v1 v2) #p v @ s; E
-  {{{ RET (v1, #true) ; ∃ pvs', ⌜pvs = ((v1, #true)%V, v)::pvs'⌝ ∗ proph p pvs' ∗ l ↦ v2 }}}.
-Proof.
-  iIntros (Hcmp Φ) "[Hp Hl] HΦ".
-  iApply (wp_resolve with "Hp"); first done.
-  assert (val_is_unboxed v1) as Hv1; first by destruct Hcmp.
-  iApply (wp_cmpxchg_suc with "Hl"); [done..|]. iIntros "!> Hl".
-  iIntros (pvs' ->) "Hp". iApply "HΦ". eauto with iFrame.
-Qed.
-
-Lemma wp_resolve_cmpxchg_fail s E l (p : proph_id) (pvs : list (val * val)) q v' v1 v2 v :
-  v' ≠ v1 → vals_compare_safe v' v1 →
-  {{{ proph p pvs ∗ ▷ l ↦{q} v' }}}
-    Resolve (CmpXchg #l v1 v2) #p v @ s; E
-  {{{ RET (v', #false) ; ∃ pvs', ⌜pvs = ((v', #false)%V, v)::pvs'⌝ ∗ proph p pvs' ∗ l ↦{q} v' }}}.
-Proof.
-  iIntros (NEq Hcmp Φ) "[Hp Hl] HΦ".
-  iApply (wp_resolve with "Hp"); first done.
-  iApply (wp_cmpxchg_fail with "Hl"); [done..|]. iIntros "!> Hl".
-  iIntros (pvs' ->) "Hp". iApply "HΦ". eauto with iFrame.
-Qed.
-
 End lifting.
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index dea83e0950224b0f60fe1ef108635fdbdaa5045b..28eae1b6f4be01417d72bd52229a1d7d5a87798e 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -1,7 +1,7 @@
 From iris.proofmode Require Import coq_tactics reduction.
 From iris.proofmode Require Export tactics.
 From iris.program_logic Require Import atomic.
-From iris.heap_lang Require Export tactics array.
+From iris.heap_lang Require Export tactics derived_laws.
 From iris.heap_lang Require Import notation.
 Set Default Proof Using "Type".
 Import uPred.
diff --git a/theories/program_logic/lifting.v b/theories/program_logic/lifting.v
index 96118502d903dc39477d8d10f640205fa8ea370b..d7e657de4c36f1049dc1dc669aaaf96687a508b2 100644
--- a/theories/program_logic/lifting.v
+++ b/theories/program_logic/lifting.v
@@ -1,3 +1,6 @@
+(** The "lifting lemmas" in this file serve to lift the rules of the operational
+semantics to the program logic. *)
+
 From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export weakestpre.
 Set Default Proof Using "Type".