diff --git a/theories/bi/derived_laws_sbi.v b/theories/bi/derived_laws_sbi.v
index d1afdc565ce02c37ad4ee57dc782157e2ac494f7..842fcdaa12403c51136789be2435a69e23b7fffd 100644
--- a/theories/bi/derived_laws_sbi.v
+++ b/theories/bi/derived_laws_sbi.v
@@ -1,6 +1,5 @@
 From iris.bi Require Export derived_laws_bi.
 From iris.algebra Require Import monoid.
-From stdpp Require Import hlist.
 
 Module bi.
 Import interface.bi.