diff --git a/Logic/FirstOrder/Arith/Model.lean b/Logic/FirstOrder/Arith/Model.lean
index 24feb893..d9b3bca5 100644
--- a/Logic/FirstOrder/Arith/Model.lean
+++ b/Logic/FirstOrder/Arith/Model.lean
@@ -1,4 +1,3 @@
-import Logic.FirstOrder.Completeness.Completeness
 import Logic.FirstOrder.Arith.Theory
 
 namespace LO
diff --git a/Logic/FirstOrder/Completeness/SearchTree.lean b/Logic/FirstOrder/Completeness/SearchTree.lean
index 191144b4..4bdbebde 100644
--- a/Logic/FirstOrder/Completeness/SearchTree.lean
+++ b/Logic/FirstOrder/Completeness/SearchTree.lean
@@ -1,4 +1,3 @@
-import Logic.FirstOrder.Basic
 import Logic.FirstOrder.Completeness.Coding
 import Logic.Vorspiel.Order
 
diff --git a/Logic/FirstOrder/Order/Le.lean b/Logic/FirstOrder/Order/Le.lean
index eaa983b7..c182e132 100644
--- a/Logic/FirstOrder/Order/Le.lean
+++ b/Logic/FirstOrder/Order/Le.lean
@@ -1,6 +1,4 @@
-import Logic.FirstOrder.Basic
 import Logic.FirstOrder.Completeness.Completeness
---import Logic.FirstOrder.Principia.Meta
 
 namespace LO
 
diff --git a/Logic/FirstOrder/Ultraproduct.lean b/Logic/FirstOrder/Ultraproduct.lean
index cb1ebf2d..788f02c1 100644
--- a/Logic/FirstOrder/Ultraproduct.lean
+++ b/Logic/FirstOrder/Ultraproduct.lean
@@ -1,4 +1,4 @@
-import Logic.FirstOrder.Basic
+import Logic.FirstOrder.Basic.Eq
 
 namespace LO
 
diff --git a/Logic/Vorspiel/W.lean b/Logic/Vorspiel/W.lean
index 6e85b893..d04a726a 100644
--- a/Logic/Vorspiel/W.lean
+++ b/Logic/Vorspiel/W.lean
@@ -1,4 +1,3 @@
-import Logic.Vorspiel.Computability
 import Logic.Vorspiel.OmegaRec
 
 attribute [-instance] WType.instEncodableWType Encodable.finPi Encodable.fintypeArrowOfEncodable