diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index 8e3e8ec207a7a4a99627a3fc33ba488228bfff9b..3dc9c1ce783ffdda4a9970cefad108e1cce18df3 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -1,7 +1,8 @@
 From iris.algebra Require Import numbers.
 From iris.proofmode Require Import tactics.
 From lrust.typing Require Export type.
-From lrust.typing Require Import type_context lft_contexts product own uniq_bor shr_bor.
+From lrust.typing Require Import type_context lft_contexts product own uniq_bor.
+From lrust.typing Require Import shr_bor.
 Set Default Proof Using "Type".
 
 Section product_split.