diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v
index 0ad6b7c5a8aa35c69506c078ee97314f1c06a0b1..71f2f7068375e48ee095a791cff6ca7e7d7505e8 100644
--- a/theories/bi/big_op.v
+++ b/theories/bi/big_op.v
@@ -2,7 +2,7 @@ From iris.algebra Require Export big_op.
 From iris.bi Require Import derived_laws_sbi plainly.
 From stdpp Require Import countable fin_collections functions.
 Set Default Proof Using "Type".
-Import interface.bi derived_laws_bi.bi.
+Import interface.bi derived_laws_bi.bi derived_laws_sbi.bi.
 
 (* Notations *)
 Notation "'[∗' 'list]' k ↦ x ∈ l , P" :=