diff --git a/theories/heap_lang/adequacy.v b/theories/heap_lang/adequacy.v
index 51529438b392a93878e3f21458f0be2b7982d7fd..9c28699974cc8596c44c1c2e31efed6dc77cdc0c 100644
--- a/theories/heap_lang/adequacy.v
+++ b/theories/heap_lang/adequacy.v
@@ -1,5 +1,4 @@
 From iris.program_logic Require Export weakestpre adequacy.
-From iris.heap_lang Require Export lifting.
 From iris.algebra Require Import auth.
 From iris.heap_lang Require Import proofmode notation.
 From iris.proofmode Require Import tactics.