diff --git a/theories/heap_lang/derived_laws.v b/theories/heap_lang/derived_laws.v
index 704c18a8e21fa1a792f485d057de09fc71b732af..1e36d1f7a9df0788677250eb80a308613c1bd529 100644
--- a/theories/heap_lang/derived_laws.v
+++ b/theories/heap_lang/derived_laws.v
@@ -1,13 +1,12 @@
-(** This file extens the HeapLang program logic with some derived laws about
-arrays and prophecies.
+(** This file extends the HeapLang program logic with some derived laws (not
+using the lifting lemmas) about arrays and prophecies.
 
-For more array operations, see [heap_lang.lib.array].
-*)
+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.program_logic Require Import ectx_lifting.
 From iris.heap_lang Require Export primitive_laws.
 From iris.heap_lang Require Import tactics notation.
 Set Default Proof Using "Type".
@@ -333,7 +332,7 @@ Lemma wp_resolve_proph s E (p : proph_id) (pvs : list (val * val)) v :
   {{{ 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.
+  iApply lifting.wp_pure_step_later=> //=. iApply wp_value.
   iIntros "!>" (vs') "HEq Hp". iApply "HΦ". iFrame.
 Qed.
 
diff --git a/theories/heap_lang/primitive_laws.v b/theories/heap_lang/primitive_laws.v
index 9fc1766cf31688a269b654b0780673a82ae75a56..047c26815ba417e2af90ddb14b55bcad456f5341 100644
--- a/theories/heap_lang/primitive_laws.v
+++ b/theories/heap_lang/primitive_laws.v
@@ -1,4 +1,5 @@
-(** This file proves the basic laws of the HeapLang program logic. *)
+(** 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.
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".