diff --git a/LeroyCompilerVerificationCourse/Compil.lean b/LeroyCompilerVerificationCourse/Compil.lean
index 1a4b0a2..9534afd 100644
--- a/LeroyCompilerVerificationCourse/Compil.lean
+++ b/LeroyCompilerVerificationCourse/Compil.lean
@@ -4,9 +4,7 @@ Released under LGPL 2.1 license as described in the file LICENSE.md.
 Authors: Wojciech Różowski
 -/
 
-import LeroyCompilerVerificationCourse.Sequences
 import LeroyCompilerVerificationCourse.Imp
-import Init.Data.List.Basic
 
 @[grind] inductive instr : Type where
   | Iconst (n: Int)
diff --git a/LeroyCompilerVerificationCourse/Constprop.lean b/LeroyCompilerVerificationCourse/Constprop.lean
index c6ac303..9f9b96a 100644
--- a/LeroyCompilerVerificationCourse/Constprop.lean
+++ b/LeroyCompilerVerificationCourse/Constprop.lean
@@ -4,11 +4,8 @@ Released under LGPL 2.1 license as described in the file LICENSE.md.
 Authors: Wojciech Różowski
 -/
 
-import LeroyCompilerVerificationCourse.Sequences
 import LeroyCompilerVerificationCourse.Imp
-import Init.Data.List.Basic
 import Std.Data.HashMap
-import Std.Data.HashMap.Lemmas
 open Classical in
 instance [BEq α] [BEq β] [Hashable α] : BEq (Std.HashMap α β) where
   beq m n := Id.run do
diff --git a/LeroyCompilerVerificationCourse/Deadcode.lean b/LeroyCompilerVerificationCourse/Deadcode.lean
index 3f27efc..40643d9 100644
--- a/LeroyCompilerVerificationCourse/Deadcode.lean
+++ b/LeroyCompilerVerificationCourse/Deadcode.lean
@@ -4,11 +4,8 @@ Released under LGPL 2.1 license as described in the file LICENSE.md.
 Authors: Wojciech Różowski
 -/
 
-import LeroyCompilerVerificationCourse.Sequences
 import LeroyCompilerVerificationCourse.Imp
-import Init.Data.List.Basic
 import Std.Data.HashSet
-import Std.Data.HashSet.Lemmas
 
 open Classical in
 @[grind] def IdentSet := Std.HashSet ident
diff --git a/LeroyCompilerVerificationCourse/Fixpoints.lean b/LeroyCompilerVerificationCourse/Fixpoints.lean
index b76586b..b7ea821 100644
--- a/LeroyCompilerVerificationCourse/Fixpoints.lean
+++ b/LeroyCompilerVerificationCourse/Fixpoints.lean
@@ -6,14 +6,7 @@ Authors: Wojciech Różowski
 
 import LeroyCompilerVerificationCourse.Imp
 import LeroyCompilerVerificationCourse.Constprop
-import Init.WF
-import Std.Data.HashMap
-import Std.Data.HashMap.Lemmas
-import Batteries.Data.List.Basic
 import Batteries.Data.List.Perm
-import Init.Data.List.Pairwise
-import Init.Data.List.Sublist
-import Init.Data.List.Basic
 
 universe u