diff --git a/Aesop/Tracing.lean b/Aesop/Tracing.lean
index 7730a5f..e5ed977 100644
--- a/Aesop/Tracing.lean
+++ b/Aesop/Tracing.lean
@@ -5,6 +5,7 @@ Authors: Jannis Limperg
 -/
 
 import Aesop.Util.Basic
+import Batteries.Data.Array.Basic
 import Lean.Elab.Term
 import Lean.Meta.Tactic.Simp
 
diff --git a/Aesop/Util/UnorderedArraySet.lean b/Aesop/Util/UnorderedArraySet.lean
index e6a0257..08b8520 100644
--- a/Aesop/Util/UnorderedArraySet.lean
+++ b/Aesop/Util/UnorderedArraySet.lean
@@ -3,7 +3,6 @@ Copyright (c) 2021 Jannis Limperg. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jannis Limperg
 -/
-import Batteries.Data.Array.Basic
 import Batteries.Data.Array.Merge
 import Lean.Message
 
@@ -131,9 +130,6 @@ def all (p : α → Bool) (s : UnorderedArraySet α) (start := 0) (stop := s.siz
     Bool :=
   s.rep.all p start stop
 
-instance : BEq (UnorderedArraySet α) where
-  beq s t := s.rep.equalSet t.rep
-
 instance [ToString α] : ToString (UnorderedArraySet α) where
   toString s := toString s.rep