diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index ad3e757193433aacfb8e4debaa9d5dff79688f0e..54eae3a5dadcf94a75edb7e9c594c00c16169a31 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -3,7 +3,7 @@ From iris.proofmode Require Import tactics.
 From iris.base_logic Require Import big_op.
 From lrust.lifetime Require Import borrow frac_borrow.
 From lrust.typing Require Export type.
-From lrust.typing Require Import typing type_context lft_contexts perm product own uniq_bor shr_bor.
+From lrust.typing Require Import type_context lft_contexts product own uniq_bor shr_bor.
 
 Section product_split.
   Context `{typeG Σ}.