diff --git a/src/Data/Tree/AVL/Map/Membership/Propositional.agda b/src/Data/Tree/AVL/Map/Membership/Propositional.agda
index 7f5151600f..c040f63a0e 100644
--- a/src/Data/Tree/AVL/Map/Membership/Propositional.agda
+++ b/src/Data/Tree/AVL/Map/Membership/Propositional.agda
@@ -13,40 +13,26 @@ module Data.Tree.AVL.Map.Membership.Propositional
   {a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂)
   where
 
-open import Data.Bool.Base using (true; false)
-open import Data.Maybe.Base using (just; nothing; is-just)
-open import Data.Product.Base using (_×_; ∃-syntax; _,_; proj₁; proj₂)
-open import Data.Product.Relation.Binary.Pointwise.NonDependent renaming (Pointwise to _×ᴿ_)
-open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
-open import Function.Base using (_∘_; _∘′_)
+open import Data.Product.Base using (_×_)
+open import Data.Product.Relation.Binary.Pointwise.NonDependent
+  using ()
+  renaming (Pointwise to _×ᴿ_)
 open import Level using (Level)
 
-open import Relation.Binary.Definitions using (Transitive; Symmetric; _Respectsˡ_)
 open import Relation.Binary.Core using (Rel)
-open import Relation.Binary.Construct.Intersection using (_∩_)
-open import Relation.Binary.PropositionalEquality.Core
-  using (_≡_; cong) renaming (refl to ≡-refl; sym to ≡-sym; trans to ≡-trans)
-open import Relation.Nullary using (Reflects; ¬_; yes; no)
-open import Relation.Nullary.Negation using (contradiction)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_)
+open import Relation.Nullary.Negation.Core using (¬_)
+
+open StrictTotalOrder strictTotalOrder using (_≈_) renaming (Carrier to Key)
+open import Data.Tree.AVL.Map strictTotalOrder using (Map)
+open import Data.Tree.AVL.Map.Relation.Unary.Any strictTotalOrder using (Any)
 
-open StrictTotalOrder strictTotalOrder renaming (Carrier to Key) hiding (trans)
-open Eq using (_≉_; refl; sym; trans)
-open import Data.Tree.AVL strictTotalOrder using (tree)
-open import Data.Tree.AVL.Indexed strictTotalOrder using (key)
-import Data.Tree.AVL.Indexed.Relation.Unary.Any strictTotalOrder as IAny
-import Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties strictTotalOrder as IAnyₚ
-open import Data.Tree.AVL.Key strictTotalOrder using (⊥⁺<[_]<⊤⁺)
-open import Data.Tree.AVL.Map strictTotalOrder
-open import Data.Tree.AVL.Map.Relation.Unary.Any strictTotalOrder as Mapₚ using (Any)
-open import Data.Tree.AVL.Relation.Unary.Any strictTotalOrder as Any using (tree)
 
 private
   variable
-    v p q : Level
+    v : Level
     V : Set v
     m : Map V
-    k k′ : Key
-    x x′ y y′ : V
     kx : Key × V
 
 infix 4 _≈ₖᵥ_