diff --git a/src/main/scala/Example.scala b/src/main/scala/Example.scala
index c66802c1fbbfb9c3eae20d798bff3e81efe3b3d1..6d4eb4ce0c8aafea649da06f3db79f9f740ded64 100644
--- a/src/main/scala/Example.scala
+++ b/src/main/scala/Example.scala
@@ -1,9 +1,10 @@
-import lisa.KernelHelpers.{*, given}
+import lisa.KernelHelpers.{_, given}
 import lisa.kernel.Printer.*
 import lisa.kernel.fol.FOL.*
+import lisa.kernel.proof.SCProof
+import lisa.kernel.proof.SCProofChecker
 import lisa.kernel.proof.SCProofChecker.*
 import lisa.kernel.proof.SequentCalculus.*
-import lisa.kernel.proof.{SCProof, SCProofChecker}
 import proven.tactics.SimplePropositionalSolver.solveSequent
 import tptp.KernelParser.*
 import tptp.ProblemGatherer.getPRPproblems
diff --git a/src/main/scala/lisa/kernel/Printer.scala b/src/main/scala/lisa/kernel/Printer.scala
index 860d5b496ecfa2b1e5c38437f8cd3b8795ae594a..3bac64702d2853550b42941c9d957aa76bec5164 100644
--- a/src/main/scala/lisa/kernel/Printer.scala
+++ b/src/main/scala/lisa/kernel/Printer.scala
@@ -1,9 +1,10 @@
 package lisa.kernel
 
 import lisa.kernel.fol.FOL.*
-import lisa.kernel.proof.SequentCalculus.*
+import lisa.kernel.proof.SCProof
+import lisa.kernel.proof.SCProofCheckerJudgement
 import lisa.kernel.proof.SCProofCheckerJudgement.*
-import lisa.kernel.proof.{SCProof, SCProofCheckerJudgement}
+import lisa.kernel.proof.SequentCalculus.*
 
 /**
  * A set of methods to pretty-print kernel trees.
diff --git a/src/main/scala/lisa/kernel/proof/RunningTheory.scala b/src/main/scala/lisa/kernel/proof/RunningTheory.scala
index 0b076bc2ff338d51c5c40220da0f122b7d7503ff..c68e8993b38a39e19e1cf9363ef50494509efabe 100644
--- a/src/main/scala/lisa/kernel/proof/RunningTheory.scala
+++ b/src/main/scala/lisa/kernel/proof/RunningTheory.scala
@@ -1,13 +1,13 @@
 package lisa.kernel.proof
 
-import lisa.kernel.proof.SequentCalculus.*
-import lisa.kernel.proof.SCProofChecker.*
 import lisa.kernel.fol.FOL.*
+import lisa.kernel.proof.RunningTheoryJudgement.*
+import lisa.kernel.proof.SCProofChecker.*
+import lisa.kernel.proof.SequentCalculus.*
 
+import scala.collection.immutable.Set
 import scala.collection.mutable.Map as mMap
 import scala.collection.mutable.Set as mSet
-import scala.collection.immutable.Set
-import lisa.kernel.proof.RunningTheoryJudgement.*
 
 /**
  * This class describes the theory, i.e. the context and language, in which theorems are proven.
diff --git a/src/main/scala/lisa/kernel/proof/SCProof.scala b/src/main/scala/lisa/kernel/proof/SCProof.scala
index f5645e55f57b1e4e008b5ccac693b5bbcf7c6ee4..65c40f8de93d2ecd1c4b20719d49e506ba8afc94 100644
--- a/src/main/scala/lisa/kernel/proof/SCProof.scala
+++ b/src/main/scala/lisa/kernel/proof/SCProof.scala
@@ -1,7 +1,7 @@
 package lisa.kernel.proof
 
-import lisa.kernel.proof.SequentCalculus._
 import lisa.kernel.proof.SCProofChecker._
+import lisa.kernel.proof.SequentCalculus._
 
 /**
  * A SCPRoof (for Sequent Calculus Proof) is a (dependant) proof. While technically a proof is an Directed Acyclic Graph,
diff --git a/src/main/scala/lisa/kernel/proof/SCProofChecker.scala b/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
index 51d92d6af65230a6ef373ca5989fd5b19a895347..ad72abfe303ef53d79351c0b4422f30b2f96961a 100644
--- a/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
+++ b/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
@@ -2,8 +2,8 @@ package lisa.kernel.proof
 
 import lisa.kernel.Printer
 import lisa.kernel.fol.FOL.*
-import lisa.kernel.proof.SequentCalculus.*
 import lisa.kernel.proof.SCProofCheckerJudgement.*
+import lisa.kernel.proof.SequentCalculus.*
 
 object SCProofChecker {
 
diff --git a/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala b/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala
index 38549206c764dc484ba270e855ea3a77c02958fd..337e67feb6c7d460d98f77577944bc79d891612d 100644
--- a/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala
+++ b/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala
@@ -1,8 +1,8 @@
 package lisa.settheory
 
+import lisa.KernelHelpers.{_, given}
 import lisa.kernel.fol.FOL._
 import lisa.kernel.proof.RunningTheory
-import lisa.KernelHelpers.{given, _}
 
 /**
  * Base trait for set theoretical axiom systems.
diff --git a/src/main/scala/lisa/settheory/SetTheoryTGAxioms.scala b/src/main/scala/lisa/settheory/SetTheoryTGAxioms.scala
index e5ba188150926cb43d76edaa18c714fad4f22296..c2bedfa3143a22afd62d46b15b791fa8f9adfd1f 100644
--- a/src/main/scala/lisa/settheory/SetTheoryTGAxioms.scala
+++ b/src/main/scala/lisa/settheory/SetTheoryTGAxioms.scala
@@ -1,6 +1,6 @@
 package lisa.settheory
+import lisa.KernelHelpers.{_, given}
 import lisa.kernel.fol.FOL._
-import lisa.KernelHelpers.{given, _}
 
 /**
  * Axioms for the Tarski-Grothendieck theory (TG)
diff --git a/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala b/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala
index 7a9ff3347b3af5d2e8de78d2754b444023113495..7c7a7d222e46dc0bd0f1a9ebd96514f272d2ac44 100644
--- a/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala
+++ b/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala
@@ -1,8 +1,8 @@
 package lisa.settheory
 
+import lisa.KernelHelpers.{_, given}
 import lisa.kernel.fol.FOL.*
 import lisa.kernel.proof.RunningTheory
-import lisa.KernelHelpers.{given, _}
 
 /**
  * Axioms for the Zermelo theory (Z)
diff --git a/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala b/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala
index 06f6aee971d604f9410e3499daa690e5ee935f30..e3648b7ee1a805ddaeb42e2881e6ea911bcbc42a 100644
--- a/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala
+++ b/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala
@@ -1,7 +1,7 @@
 package lisa.settheory
 
+import lisa.KernelHelpers.{_, given}
 import lisa.kernel.fol.FOL._
-import lisa.KernelHelpers.{given, _}
 
 /**
  * Axioms for the Zermelo-Fraenkel theory (ZF)
diff --git a/src/main/scala/proven/DSetTheory/Part1.scala b/src/main/scala/proven/DSetTheory/Part1.scala
index e04d1b98485de34bb227a0bef7bc9830f9129089..b82f09ff37a5b29a9ef59a418ef9d42ad0fe82c2 100644
--- a/src/main/scala/proven/DSetTheory/Part1.scala
+++ b/src/main/scala/proven/DSetTheory/Part1.scala
@@ -1,20 +1,22 @@
 package proven.DSetTheory
-import lisa.kernel.fol.FOL.*
-import lisa.kernel.proof.SequentCalculus.*
-import lisa.KernelHelpers.{*, given}
+import lisa.KernelHelpers.{_, given}
 import lisa.kernel.Printer
-import lisa.kernel.Printer.{prettyFormula, prettySCProof}
+import lisa.kernel.Printer.prettyFormula
+import lisa.kernel.Printer.prettySCProof
 import lisa.kernel.fol.FOL
-import proven.tactics.ProofTactics.*
-import proven.tactics.Destructors.*
-import lisa.settheory.AxiomaticSetTheory.*
-import proven.ElementsOfSetTheory.{oPair, orderedPairDefinition}
-
-import scala.collection.immutable.SortedSet
-import lisa.kernel.proof.{SCProof, SCProofChecker}
+import lisa.kernel.fol.FOL.*
+import lisa.kernel.proof.SCProof
+import lisa.kernel.proof.SCProofChecker
+import lisa.kernel.proof.SequentCalculus.*
 import lisa.settheory.AxiomaticSetTheory
+import lisa.settheory.AxiomaticSetTheory.*
+import proven.ElementsOfSetTheory.oPair
+import proven.ElementsOfSetTheory.orderedPairDefinition
+import proven.tactics.Destructors.*
+import proven.tactics.ProofTactics.*
 
 import scala.collection.immutable
+import scala.collection.immutable.SortedSet
 object Part1 {
   val theory = AxiomaticSetTheory.runningSetTheory
   def axiom(f: Formula): theory.Axiom = theory.getAxiom(f).get
diff --git a/src/main/scala/proven/ElementsOfSetTheory.scala b/src/main/scala/proven/ElementsOfSetTheory.scala
index 288cdbf5024d5bf22e1f83ee93ef6a9b96aa30ad..52934b109d6b153840f66e921c5c79eeaad1592d 100644
--- a/src/main/scala/proven/ElementsOfSetTheory.scala
+++ b/src/main/scala/proven/ElementsOfSetTheory.scala
@@ -1,18 +1,18 @@
 package proven
+import lisa.KernelHelpers.{_, given}
+import lisa.kernel.Printer
 import lisa.kernel.fol.FOL.*
+import lisa.kernel.proof.SCProof
+import lisa.kernel.proof.SCProofChecker
 import lisa.kernel.proof.SequentCalculus.*
-import lisa.KernelHelpers.{*, given}
-import lisa.kernel.Printer
-import proven.tactics.ProofTactics.*
-import proven.tactics.Destructors.*
-import lisa.settheory.AxiomaticSetTheory.*
-
-import scala.collection.immutable.SortedSet
-import lisa.kernel.proof.{SCProof, SCProofChecker}
 import lisa.settheory.AxiomaticSetTheory
+import lisa.settheory.AxiomaticSetTheory.*
 import proven.ElementsOfSetTheory.theory
+import proven.tactics.Destructors.*
+import proven.tactics.ProofTactics.*
 
 import scala.collection.immutable
+import scala.collection.immutable.SortedSet
 
 /**
  * Some proofs in set theory. See it as a proof of concept.
diff --git a/src/main/scala/proven/tactics/Destructors.scala b/src/main/scala/proven/tactics/Destructors.scala
index 6827746229ac47585fc9a5d1ca4acc1a37d1ec3a..36f53f3f6a5cfc00667e7b91abfec3b9223d0367 100644
--- a/src/main/scala/proven/tactics/Destructors.scala
+++ b/src/main/scala/proven/tactics/Destructors.scala
@@ -1,10 +1,10 @@
 package proven.tactics
 
-import lisa.kernel.proof.SequentCalculus.*
-import lisa.kernel.fol.FOL.*
 import lisa.KernelHelpers.*
-import proven.tactics.ProofTactics.hypothesis
+import lisa.kernel.fol.FOL.*
 import lisa.kernel.proof.SCProof
+import lisa.kernel.proof.SequentCalculus.*
+import proven.tactics.ProofTactics.hypothesis
 
 object Destructors {
   def destructRightOr(p: SCProof, a: Formula, b: Formula): SCProof = {
diff --git a/src/main/scala/proven/tactics/ProofTactics.scala b/src/main/scala/proven/tactics/ProofTactics.scala
index 8fe34fad98ee41029d95b113859cbd21efa7803f..191e77a1a4ba440723959a1e51b0af10be7b2de8 100644
--- a/src/main/scala/proven/tactics/ProofTactics.scala
+++ b/src/main/scala/proven/tactics/ProofTactics.scala
@@ -1,12 +1,12 @@
 package proven.tactics
 
+import lisa.KernelHelpers.{_, given}
+import lisa.kernel.Printer.*
 import lisa.kernel.fol.FOL.*
+import lisa.kernel.proof.SCProof
 import lisa.kernel.proof.SequentCalculus.*
-import lisa.KernelHelpers.{*, given}
-import lisa.kernel.Printer.*
 
 import scala.collection.immutable.Set
-import lisa.kernel.proof.SCProof
 
 /**
  * SCProof tactics are a set of strategies that help the user write proofs in a more expressive way
diff --git a/src/main/scala/proven/tactics/SimplePropositionalSolver.scala b/src/main/scala/proven/tactics/SimplePropositionalSolver.scala
index 7d45e9d71ab8f5488cef1ad3f80513d07f31e19d..50d87de5df78fe040405d32ec84154d76cb71c41 100644
--- a/src/main/scala/proven/tactics/SimplePropositionalSolver.scala
+++ b/src/main/scala/proven/tactics/SimplePropositionalSolver.scala
@@ -1,10 +1,11 @@
 package proven.tactics
 
+import lisa.KernelHelpers.*
 import lisa.kernel.fol.FOL.*
+import lisa.kernel.proof.SCProof
 import lisa.kernel.proof.SequentCalculus.*
+
 import scala.collection.mutable.Set as mSet
-import lisa.KernelHelpers.*
-import lisa.kernel.proof.SCProof
 
 /**
  * A simple but complete solver for propositional logic. Will not terminate for large problems
diff --git a/src/main/scala/tptp/KernelParser.scala b/src/main/scala/tptp/KernelParser.scala
index 83485b3d0fb512980d0fedb506dc889d1dd5a383..149453e368f7dd8b3011b8d631c7004c937d60b3 100644
--- a/src/main/scala/tptp/KernelParser.scala
+++ b/src/main/scala/tptp/KernelParser.scala
@@ -1,16 +1,18 @@
 package tptp
 
-import leo.modules.input.TPTPParser as Parser
-import Parser.TPTPParseException
 import leo.datastructures.TPTP
-import leo.datastructures.TPTP.{CNF, FOF}
+import leo.datastructures.TPTP.CNF
+import leo.datastructures.TPTP.FOF
+import leo.modules.input.TPTPParser as Parser
+import lisa.KernelHelpers.*
 import lisa.kernel.fol.FOL as K
 import lisa.kernel.proof.SequentCalculus as SK
-import lisa.KernelHelpers.*
 
 import java.io.File
 import scala.util.matching.Regex
 
+import Parser.TPTPParseException
+
 object KernelParser {
 
   case class AnnotatedFormula(role: String, name: String, formula: K.Formula)
diff --git a/src/test/scala/lisa/kernel/EquivalenceCheckerTests.scala b/src/test/scala/lisa/kernel/EquivalenceCheckerTests.scala
index 722d2c1f45cb72a48c0acee966888fc6e279657c..f8ee2a8cce949bde472c35ccf6255b72bf3af0ca 100644
--- a/src/test/scala/lisa/kernel/EquivalenceCheckerTests.scala
+++ b/src/test/scala/lisa/kernel/EquivalenceCheckerTests.scala
@@ -7,7 +7,8 @@ import lisa.kernel.fol.FOL.*
 import org.scalatest.funsuite.AnyFunSuite
 
 import scala.collection.MapView
-import scala.collection.mutable.{ArrayBuffer, ListBuffer}
+import scala.collection.mutable.ArrayBuffer
+import scala.collection.mutable.ListBuffer
 import scala.util.Random
 
 class EquivalenceCheckerTests extends AnyFunSuite {
diff --git a/src/test/scala/lisa/kernel/FolTests.scala b/src/test/scala/lisa/kernel/FolTests.scala
index 27a3eede291b31d6faff676c6b7c6ff04baff8a1..8f02688c47d5fd1ac6b438ca7dd967bc50d5f16f 100644
--- a/src/test/scala/lisa/kernel/FolTests.scala
+++ b/src/test/scala/lisa/kernel/FolTests.scala
@@ -1,13 +1,14 @@
 package lisa.kernel
 
-import lisa.KernelHelpers.{*, given}
+import lisa.KernelHelpers.{_, given}
 import lisa.kernel.Printer
-import lisa.kernel.proof.RunningTheory
-import org.scalatest.funsuite.AnyFunSuite
-import lisa.kernel.proof.SequentCalculus.*
 import lisa.kernel.fol.FOL.*
+import lisa.kernel.proof.RunningTheory
 import lisa.kernel.proof.RunningTheory.*
-import lisa.kernel.proof.{SCProof, SCProofChecker}
+import lisa.kernel.proof.SCProof
+import lisa.kernel.proof.SCProofChecker
+import lisa.kernel.proof.SequentCalculus.*
+import org.scalatest.funsuite.AnyFunSuite
 
 import scala.collection.immutable.SortedSet
 import scala.util.Random
diff --git a/src/test/scala/lisa/kernel/PrinterTest.scala b/src/test/scala/lisa/kernel/PrinterTest.scala
index 23edf5a24b16f47616809d8c9171255976e4800b..cf6a4899b65440498135e5996e7a7547791543eb 100644
--- a/src/test/scala/lisa/kernel/PrinterTest.scala
+++ b/src/test/scala/lisa/kernel/PrinterTest.scala
@@ -1,8 +1,7 @@
 package lisa.kernel
 
-import lisa.kernel.fol.FOL._
 import lisa.kernel.Printer._
-
+import lisa.kernel.fol.FOL._
 import org.scalatest.funsuite.AnyFunSuite
 
 class PrinterTest extends AnyFunSuite {
diff --git a/src/test/scala/lisa/kernel/ProofTests.scala b/src/test/scala/lisa/kernel/ProofTests.scala
index 665f95754322cdbba1a9b75a8641453856986206..07b5a3a0718138d44c59d7c990589cdb748d89d8 100644
--- a/src/test/scala/lisa/kernel/ProofTests.scala
+++ b/src/test/scala/lisa/kernel/ProofTests.scala
@@ -1,13 +1,14 @@
 package lisa.kernel
 
-import lisa.KernelHelpers.{*, given}
+import lisa.KernelHelpers.{_, given}
 import lisa.kernel.Printer
-import lisa.kernel.proof.RunningTheory
-import org.scalatest.funsuite.AnyFunSuite
-import lisa.kernel.proof.SequentCalculus.*
 import lisa.kernel.fol.FOL.*
+import lisa.kernel.proof.RunningTheory
 import lisa.kernel.proof.RunningTheory.*
-import lisa.kernel.proof.{SCProof, SCProofChecker}
+import lisa.kernel.proof.SCProof
+import lisa.kernel.proof.SCProofChecker
+import lisa.kernel.proof.SequentCalculus.*
+import org.scalatest.funsuite.AnyFunSuite
 
 import scala.util.Random
 
diff --git a/src/test/scala/lisa/proven/ElementsOfSetTheoryTests.scala b/src/test/scala/lisa/proven/ElementsOfSetTheoryTests.scala
index 5786462d0495fa3aeb214878b01718d01bc6bbfa..98ade22df1a34052e455ad71246b4d26573dfec0 100644
--- a/src/test/scala/lisa/proven/ElementsOfSetTheoryTests.scala
+++ b/src/test/scala/lisa/proven/ElementsOfSetTheoryTests.scala
@@ -1,15 +1,15 @@
 package proven
 
+import lisa.KernelHelpers.{_, given}
 import lisa.kernel.Printer
-import lisa.settheory.AxiomaticSetTheory.*
-import test.ProofCheckerSuite
-import proven.tactics.ProofTactics
+import lisa.kernel.fol.FOL.*
 import lisa.kernel.proof.SCProof
-import proven.ElementsOfSetTheory.*
 import lisa.kernel.proof.SequentCalculus.Sequent
-import lisa.kernel.fol.FOL.*
-import lisa.KernelHelpers.{*, given}
 import lisa.kernel.proof.SequentCalculus.*
+import lisa.settheory.AxiomaticSetTheory.*
+import proven.ElementsOfSetTheory.*
+import proven.tactics.ProofTactics
+import test.ProofCheckerSuite
 
 class ElementsOfSetTheoryTests extends ProofCheckerSuite {
 
diff --git a/src/test/scala/lisa/proven/SimpleProverTests.scala b/src/test/scala/lisa/proven/SimpleProverTests.scala
index 8f56fe7be3442b98d4195b0360b9025894c4e15f..9731249f967d98ba67d54776dfbdb3990f48774b 100644
--- a/src/test/scala/lisa/proven/SimpleProverTests.scala
+++ b/src/test/scala/lisa/proven/SimpleProverTests.scala
@@ -1,15 +1,16 @@
 package proven
 
-import lisa.kernel.Printer.*
-import lisa.kernel.proof.{RunningTheory, SCProofChecker}
-import lisa.kernel.fol.FOL.*
 import lisa.KernelHelpers.*
 import lisa.kernel.Printer
+import lisa.kernel.Printer.*
+import lisa.kernel.fol.FOL.*
+import lisa.kernel.proof.RunningTheory
 import lisa.kernel.proof.RunningTheory.PredicateLogic
+import lisa.kernel.proof.SCProofChecker
 import org.scalatest.funsuite.AnyFunSuite
-import tptp.ProblemGatherer.getPRPproblems
-import tptp.KernelParser.*
 import proven.tactics.SimplePropositionalSolver as SPS
+import tptp.KernelParser.*
+import tptp.ProblemGatherer.getPRPproblems
 
 class SimpleProverTests extends AnyFunSuite {
 
diff --git a/src/test/scala/test/ProofCheckerSuite.scala b/src/test/scala/test/ProofCheckerSuite.scala
index d91d1fd9a1761af03d847ed93fea4ca7c4448c2d..8a5961861d983936260560f92ababa61b462ef2d 100644
--- a/src/test/scala/test/ProofCheckerSuite.scala
+++ b/src/test/scala/test/ProofCheckerSuite.scala
@@ -1,13 +1,14 @@
 package test
 
+import lisa.KernelHelpers._
+import lisa.KernelHelpers.given_Conversion_Boolean_List_String_Option
 import lisa.kernel.Printer
-import lisa.kernel.proof.SequentCalculus.{Sequent, isSameSequent}
+import lisa.kernel.proof.SCProof
 import lisa.kernel.proof.SCProofChecker._
+import lisa.kernel.proof.SequentCalculus.Sequent
+import lisa.kernel.proof.SequentCalculus.isSameSequent
 import lisa.settheory.AxiomaticSetTheory
 import org.scalatest.funsuite.AnyFunSuite
-import lisa.kernel.proof.SCProof
-import lisa.KernelHelpers._
-import lisa.KernelHelpers.given_Conversion_Boolean_List_String_Option
 
 abstract class ProofCheckerSuite extends AnyFunSuite {
   import lisa.kernel.fol.FOL.*