diff --git a/src/main/scala/Example.scala b/src/main/scala/Example.scala
index 8e7eb102fbafd9be5faccbe6144d829251f1cd24..49a5bf92ffff0b5f1e26d4bb7bea2468b88e3c87 100644
--- a/src/main/scala/Example.scala
+++ b/src/main/scala/Example.scala
@@ -1,7 +1,3 @@
-import utilities.KernelHelpers.{_, given}
-import utilities.tptp.ProblemGatherer.*
-import utilities.tptp.KernelParser.*
-import utilities.tptp.*
 import lisa.kernel.Printer.*
 import lisa.kernel.fol.FOL.*
 import lisa.kernel.proof.SCProof
@@ -9,6 +5,10 @@ import lisa.kernel.proof.SCProofChecker
 import lisa.kernel.proof.SCProofChecker.*
 import lisa.kernel.proof.SequentCalculus.*
 import proven.tactics.SimplePropositionalSolver.solveSequent
+import utilities.KernelHelpers.{_, given}
+import utilities.tptp.KernelParser.*
+import utilities.tptp.ProblemGatherer.*
+import utilities.tptp.*
 
 /**
  * Discover some of the elements of LISA to get started.
diff --git a/src/main/scala/lisa/kernel/proof/RunningTheory.scala b/src/main/scala/lisa/kernel/proof/RunningTheory.scala
index 49e6e1a09fa6b1a9a68e8e7bf44e63c258e1fbda..70f54f3c8ef1bf39d828f65d0bc4d082229503c3 100644
--- a/src/main/scala/lisa/kernel/proof/RunningTheory.scala
+++ b/src/main/scala/lisa/kernel/proof/RunningTheory.scala
@@ -77,7 +77,7 @@ class RunningTheory {
    * @param proof The proof of the desired Theorem.
    * @return A Theorem if the proof is correct, None else
    */
-  def makeTheorem(name: String, statement:Sequent, proof: SCProof, justifications: Seq[Justification]): RunningTheoryJudgement[this.Theorem] = {
+  def makeTheorem(name: String, statement: Sequent, proof: SCProof, justifications: Seq[Justification]): RunningTheoryJudgement[this.Theorem] = {
     if (proof.conclusion == statement) proofToTheorem(name, proof, justifications)
     else InvalidJustification("The proof does not prove the claimed statement", None)
   }
diff --git a/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala b/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala
index 3f630ed232c799316a9fc5cbbdeb0d52db91770e..cb030de9e9c2c4b51b05155aa472ebd5571ad3dc 100644
--- a/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala
+++ b/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala
@@ -2,7 +2,7 @@ package lisa.settheory
 
 import lisa.kernel.fol.FOL._
 import lisa.kernel.proof.RunningTheory
-import utilities.KernelHelpers.{given, _}
+import utilities.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 12fcff5c645b5fefcb3a824ff3f24b45a8ab645f..6bd499c09a36a31806a92614699e05dea8ee4db0 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.kernel.fol.FOL._
-import utilities.KernelHelpers.{given, _}
+import utilities.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 da11ebd906918d378cff11dbb4bb936a886ec022..5a47aad939e8c2afd84ad1f154820f7b308990b1 100644
--- a/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala
+++ b/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala
@@ -2,7 +2,7 @@ package lisa.settheory
 
 import lisa.kernel.fol.FOL.*
 import lisa.kernel.proof.RunningTheory
-import utilities.KernelHelpers.{given, _}
+import utilities.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 24271f812566fe17be9c4ccde566a66e13d7876e..13221cc12f60f84b53fae1d358bb3d602919001a 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.kernel.fol.FOL._
-import utilities.KernelHelpers.{given, _}
+import utilities.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 20e8e8af9f24699d1411c72e55823ec9925cf954..3d674ce858f4fd76b1d2005003dffcb54e1052a1 100644
--- a/src/main/scala/proven/DSetTheory/Part1.scala
+++ b/src/main/scala/proven/DSetTheory/Part1.scala
@@ -1,8 +1,8 @@
 package proven.DSetTheory
-import utilities.KernelHelpers.{_, given}
-import utilities.TheoriesHelpers.{*, given}
 import lisa.kernel.Printer
-import lisa.kernel.Printer.{prettyFormula, prettySCProof, prettySequent}
+import lisa.kernel.Printer.prettyFormula
+import lisa.kernel.Printer.prettySCProof
+import lisa.kernel.Printer.prettySequent
 import lisa.kernel.fol.FOL
 import lisa.kernel.fol.FOL.*
 import lisa.kernel.proof.SCProof
@@ -14,6 +14,8 @@ import proven.ElementsOfSetTheory.oPair
 import proven.ElementsOfSetTheory.orderedPairDefinition
 import proven.tactics.Destructors.*
 import proven.tactics.ProofTactics.*
+import utilities.KernelHelpers.{_, given}
+import utilities.TheoriesHelpers.{_, given}
 
 import scala.collection.immutable
 import scala.collection.immutable.SortedSet
@@ -306,12 +308,14 @@ object Part1 {
     SCProof(steps, Vector(i1, i2, i3))
   }
   println(prettySequent(thmMapFunctional.conclusion))
-  val thm_thmMapFunctional = theory.theorem("thmMapFunctional",
-    "∀a. (a ∈ ?A) ⇒ ∃!x. ?phi(x, a) ⊢ ∃!X. ∀x. (x ∈ X) ↔ ∃a. (a ∈ ?A) ∧ ?phi(x, a)",
-    thmMapFunctional,
-    Seq(axiom(replacementSchema),
-      axiom(comprehensionSchema), axiom(extensionalityAxiom))
-  ).get
+  val thm_thmMapFunctional = theory
+    .theorem(
+      "thmMapFunctional",
+      "∀a. (a ∈ ?A) ⇒ ∃!x. ?phi(x, a) ⊢ ∃!X. ∀x. (x ∈ X) ↔ ∃a. (a ∈ ?A) ∧ ?phi(x, a)",
+      thmMapFunctional,
+      Seq(axiom(replacementSchema), axiom(comprehensionSchema), axiom(extensionalityAxiom))
+    )
+    .get
 
   /**
    * ∀ b. (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b)    |-    ∃!X. ∀x. (x ∈ X) ↔ ∃b. (b ∈ B) ∧ ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ A) ∧ ?psi(x1, a, b)
@@ -382,12 +386,14 @@ object Part1 {
     // have ∀b. (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b)    |-    ∃!X. ∀x. (x ∈ X) ↔ ∃b. (b ∈ B) ∧ ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ A) ∧ ?psi(x1, a, b)   s7
   }
   println(prettySequent(lemma1.conclusion))
-  val thm_lemma1 = theory.theorem(
-    "lemma1",
-    "∀b. (b ∈ ?B) ⇒ ∀a. (a ∈ ?A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∃!X. ∀x. (x ∈ X) ↔ ∃b. (b ∈ ?B) ∧ ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ ?A) ∧ ?psi(x1, a, b)",
-    lemma1,
-    Seq(thm_thmMapFunctional)
-  ).get
+  val thm_lemma1 = theory
+    .theorem(
+      "lemma1",
+      "∀b. (b ∈ ?B) ⇒ ∀a. (a ∈ ?A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∃!X. ∀x. (x ∈ X) ↔ ∃b. (b ∈ ?B) ∧ ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ ?A) ∧ ?psi(x1, a, b)",
+      lemma1,
+      Seq(thm_thmMapFunctional)
+    )
+    .get
 
   /*
     val lemma2 = SCProof({
@@ -501,12 +507,14 @@ object Part1 {
     SCProof(Vector(s0, s1, s2), Vector(i1, i2))
   }
   println(prettySequent(lemmaMapTwoArguments.conclusion))
-  val thm_lemmaMapTwoArguments = theory.theorem(
-    "lemmaMapTwoArguments",
-    "∀b. (b ∈ ?B) ⇒ ∀a. (a ∈ ?A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∃!z. ∃x. (z = U(x)) ∧ ∀x_0. (x_0 ∈ x) ↔ ∃b. (b ∈ ?B) ∧ ∀x1. (x1 ∈ x_0) ↔ ∃a. (a ∈ ?A) ∧ ?psi(x1, a, b)",
-    lemmaMapTwoArguments,
-    Seq(thm_lemma1, thm_lemmaApplyFToObject)
-  ).get
+  val thm_lemmaMapTwoArguments = theory
+    .theorem(
+      "lemmaMapTwoArguments",
+      "∀b. (b ∈ ?B) ⇒ ∀a. (a ∈ ?A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∃!z. ∃x. (z = U(x)) ∧ ∀x_0. (x_0 ∈ x) ↔ ∃b. (b ∈ ?B) ∧ ∀x1. (x1 ∈ x_0) ↔ ∃a. (a ∈ ?A) ∧ ?psi(x1, a, b)",
+      lemmaMapTwoArguments,
+      Seq(thm_lemma1, thm_lemmaApplyFToObject)
+    )
+    .get
 
   /**
    *  ⊢ ∃!z. ∃x. (z = U(x)) ∧ ∀x_0. (x_0 ∈ x) ↔ ∃b. (b ∈ ?B) ∧ ∀x1. (x1 ∈ x_0) ↔ ∃a. (a ∈ ?A) ∧ (x1 = (a, b))
diff --git a/src/main/scala/proven/ElementsOfSetTheory.scala b/src/main/scala/proven/ElementsOfSetTheory.scala
index e39d29e95b1fe3266657de96434c5b47465ed27b..c1fd97c4000bee26b07bb7cd885d3a5a41d2396f 100644
--- a/src/main/scala/proven/ElementsOfSetTheory.scala
+++ b/src/main/scala/proven/ElementsOfSetTheory.scala
@@ -1,24 +1,20 @@
 package proven
 import lisa.kernel.Printer
+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 utilities.KernelHelpers.{*, given}
-import utilities.TheoriesHelpers.{*, given}
-import lisa.kernel.Printer
-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 lisa.settheory.AxiomaticSetTheory.*
 import proven.ElementsOfSetTheory.theory
 import proven.tactics.Destructors.*
+import proven.tactics.Destructors.*
+import proven.tactics.ProofTactics.*
 import proven.tactics.ProofTactics.*
+import utilities.KernelHelpers.{_, given}
+import utilities.TheoriesHelpers.{_, given}
 
 import scala.collection.immutable
 import scala.collection.immutable.SortedSet
@@ -77,7 +73,8 @@ object ElementsOfSetTheory {
     fin4.copy(imports = imps)
   } //   |- ∀∀({x$1,y$2}={y$2,x$1})
   println(prettySequent(proofUnorderedPairSymmetry.conclusion))
-  val thm_proofUnorderedPairSymmetry: theory.Theorem = theory.theorem("proofUnorderedPairSymmetry", "⊢ ∀y, x. {x, y} = {y, x}", proofUnorderedPairSymmetry, Seq(axiom(extensionalityAxiom), axiom(pairAxiom))).get
+  val thm_proofUnorderedPairSymmetry: theory.Theorem =
+    theory.theorem("proofUnorderedPairSymmetry", "⊢ ∀y, x. {x, y} = {y, x}", proofUnorderedPairSymmetry, Seq(axiom(extensionalityAxiom), axiom(pairAxiom))).get
 
   val proofUnorderedPairDeconstruction: SCProof = {
     val pxy = pair(x, y)
@@ -328,7 +325,14 @@ object ElementsOfSetTheory {
     generalizeToForall(SCProof(IndexedSeq(p0, p1, p2), IndexedSeq(() |- pairAxiom)), x, y, x1, y1)
   } // |- ∀∀∀∀(({x$4,y$3}={x'$2,y'$1})⇒(((y'$1=y$3)∧(x'$2=x$4))∨((x$4=y'$1)∧(y$3=x'$2))))
   println(prettySequent(proofUnorderedPairDeconstruction.conclusion))
-  val thm_proofUnorderedPairDeconstruction = theory.theorem("proofUnorderedPairDeconstruction", "⊢ ∀x, y, x', y'. ({x, y} = {x', y'}) ⇒ (y' = y) ∧ (x' = x) ∨ (x = y') ∧ (y = x')", proofUnorderedPairDeconstruction, Seq(axiom(pairAxiom))).get
+  val thm_proofUnorderedPairDeconstruction = theory
+    .theorem(
+      "proofUnorderedPairDeconstruction",
+      "⊢ ∀x, y, x', y'. ({x, y} = {x', y'}) ⇒ (y' = y) ∧ (x' = x) ∨ (x = y') ∧ (y = x')",
+      proofUnorderedPairDeconstruction,
+      Seq(axiom(pairAxiom))
+    )
+    .get
 
   // i2, i1, p0, p1, p2, p3
 
diff --git a/src/main/scala/proven/tactics/Destructors.scala b/src/main/scala/proven/tactics/Destructors.scala
index 396c6caa0f91fc4e3ae91df79816ffacf07c92a7..86fdd967d7c9383e43e1cb964f79f90e6b8cbdb2 100644
--- a/src/main/scala/proven/tactics/Destructors.scala
+++ b/src/main/scala/proven/tactics/Destructors.scala
@@ -1,12 +1,11 @@
 package proven.tactics
 
-import lisa.kernel.proof.SequentCalculus.*
 import lisa.kernel.fol.FOL.*
-import utilities.KernelHelpers.*
-import proven.tactics.ProofTactics.hypothesis
 import lisa.kernel.proof.SCProof
 import lisa.kernel.proof.SequentCalculus.*
+import lisa.kernel.proof.SequentCalculus.*
 import proven.tactics.ProofTactics.hypothesis
+import utilities.KernelHelpers.*
 
 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 bd90e0a72f69f6cdd721aada6a1a0443aad9f597..50b4d61a962826d74b41eec90a03b8e13be4e080 100644
--- a/src/main/scala/proven/tactics/ProofTactics.scala
+++ b/src/main/scala/proven/tactics/ProofTactics.scala
@@ -4,8 +4,7 @@ import lisa.kernel.Printer.*
 import lisa.kernel.fol.FOL.*
 import lisa.kernel.proof.SCProof
 import lisa.kernel.proof.SequentCalculus.*
-import utilities.KernelHelpers.{*, given}
-import lisa.kernel.Printer.*
+import utilities.KernelHelpers.{_, given}
 
 import scala.collection.immutable.Set
 
diff --git a/src/main/scala/proven/tactics/SimplePropositionalSolver.scala b/src/main/scala/proven/tactics/SimplePropositionalSolver.scala
index 87b85b602d7a0e93f151984deab8b61d8a314533..a48c558fed8dbe7f1c7de0ba64bdad2d2fc8f3ea 100644
--- a/src/main/scala/proven/tactics/SimplePropositionalSolver.scala
+++ b/src/main/scala/proven/tactics/SimplePropositionalSolver.scala
@@ -3,10 +3,9 @@ package proven.tactics
 import lisa.kernel.fol.FOL.*
 import lisa.kernel.proof.SCProof
 import lisa.kernel.proof.SequentCalculus.*
+import utilities.KernelHelpers.*
 
 import scala.collection.mutable.Set as mSet
-import utilities.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/utilities/KernelHelpers.scala b/src/main/scala/utilities/KernelHelpers.scala
index 73650c9656e194615e15878766253681e4467e5c..2e7ac7364a3e23b52d8f79683a01cf8f5cbb7bdd 100644
--- a/src/main/scala/utilities/KernelHelpers.scala
+++ b/src/main/scala/utilities/KernelHelpers.scala
@@ -1,8 +1,11 @@
 package utilities
 
+import lisa.kernel.proof.RunningTheory
+import lisa.kernel.proof.RunningTheoryJudgement
 import lisa.kernel.proof.RunningTheoryJudgement.InvalidJustification
-import lisa.kernel.proof.{RunningTheory, RunningTheoryJudgement, SCProof}
-import lisa.kernel.proof.SequentCalculus.{Rewrite, isSameSequent}
+import lisa.kernel.proof.SCProof
+import lisa.kernel.proof.SequentCalculus.Rewrite
+import lisa.kernel.proof.SequentCalculus.isSameSequent
 
 /**
  * A helper file that provides various syntactic sugars for LISA.
@@ -140,5 +143,5 @@ object KernelHelpers {
   def instantiateFunctionSchemaInSequent(s: Sequent, m: Map[SchematicFunctionLabel, LambdaTermTerm]): Sequent = {
     s.left.map(phi => instantiateFunctionSchemas(phi, m)) |- s.right.map(phi => instantiateFunctionSchemas(phi, m))
   }
-  
+
 }
diff --git a/src/main/scala/utilities/TheoriesHelpers.scala b/src/main/scala/utilities/TheoriesHelpers.scala
index 2040ba0583d914a08ed5251b87f3633cb4486f8d..e0f9864e76803c937d3dd528cc121170203bc497 100644
--- a/src/main/scala/utilities/TheoriesHelpers.scala
+++ b/src/main/scala/utilities/TheoriesHelpers.scala
@@ -1,22 +1,21 @@
 package utilities
 
+import lisa.kernel.proof.RunningTheory
+import lisa.kernel.proof.RunningTheoryJudgement
 import lisa.kernel.proof.RunningTheoryJudgement.InvalidJustification
-import lisa.kernel.proof.{RunningTheory, RunningTheoryJudgement, SCProof}
-import lisa.kernel.proof.SequentCalculus.{Rewrite, isSameSequent}
+import lisa.kernel.proof.SCProof
+import lisa.kernel.proof.SequentCalculus.Rewrite
+import lisa.kernel.proof.SequentCalculus.isSameSequent
 
 object TheoriesHelpers {
 
   // for when the kernel will have a dedicated parser
   extension (theory: RunningTheory)
-    def theorem(name: String, statement:String, proof: SCProof, justifications: Seq[theory.Justification]): RunningTheoryJudgement[theory.Theorem] = {
-      val expected = proof.conclusion  // parse(statement)
-      if ( expected == proof.conclusion) theory.makeTheorem(name, expected, proof, justifications)
-      else if (isSameSequent(expected, proof.conclusion)) theory.makeTheorem(name, expected, proof.appended(Rewrite(expected, proof.length-1)), justifications)
+    def theorem(name: String, statement: String, proof: SCProof, justifications: Seq[theory.Justification]): RunningTheoryJudgement[theory.Theorem] = {
+      val expected = proof.conclusion // parse(statement)
+      if (expected == proof.conclusion) theory.makeTheorem(name, expected, proof, justifications)
+      else if (isSameSequent(expected, proof.conclusion)) theory.makeTheorem(name, expected, proof.appended(Rewrite(expected, proof.length - 1)), justifications)
       else InvalidJustification("The proof does not prove the claimed statement", None)
     }
 
-
-
-
-
 }
diff --git a/src/main/scala/utilities/tptp/KernelParser.scala b/src/main/scala/utilities/tptp/KernelParser.scala
index 036242c53fb52a7e3a0a35113b468b71419f8f9e..3f7d2fe05c1c40c482291212c7bb75cf2c6d9f35 100644
--- a/src/main/scala/utilities/tptp/KernelParser.scala
+++ b/src/main/scala/utilities/tptp/KernelParser.scala
@@ -3,11 +3,11 @@ package utilities.tptp
 import leo.datastructures.TPTP
 import leo.datastructures.TPTP.CNF
 import leo.datastructures.TPTP.FOF
-import utilities.tptp.*
 import leo.modules.input.TPTPParser as Parser
 import lisa.kernel.fol.FOL as K
 import lisa.kernel.proof.SequentCalculus as LK
 import utilities.KernelHelpers.*
+import utilities.tptp.*
 
 import java.io.File
 import scala.util.matching.Regex
diff --git a/src/test/scala/lisa/kernel/EquivalenceCheckerTests.scala b/src/test/scala/lisa/kernel/EquivalenceCheckerTests.scala
index 518ce3f9d2897d668fccc041227fdeb00987b591..2576c9c9a4863c35b97ee62760b0ff958ea14bf2 100644
--- a/src/test/scala/lisa/kernel/EquivalenceCheckerTests.scala
+++ b/src/test/scala/lisa/kernel/EquivalenceCheckerTests.scala
@@ -1,10 +1,10 @@
 package lisa.kernel
 
-import utilities.KernelHelpers.*
 import lisa.kernel.Printer
 import lisa.kernel.fol.FOL
 import lisa.kernel.fol.FOL.*
 import org.scalatest.funsuite.AnyFunSuite
+import utilities.KernelHelpers.*
 
 import scala.collection.MapView
 import scala.collection.mutable.ArrayBuffer
diff --git a/src/test/scala/lisa/kernel/FolTests.scala b/src/test/scala/lisa/kernel/FolTests.scala
index 615d58e1954d3db2f8611d49e83e011579860c07..7ebe445cc788ee09fb913207d4f049260dede3ba 100644
--- a/src/test/scala/lisa/kernel/FolTests.scala
+++ b/src/test/scala/lisa/kernel/FolTests.scala
@@ -1,6 +1,5 @@
 package lisa.kernel
 
-import utilities.KernelHelpers.{_, given}
 import lisa.kernel.Printer
 import lisa.kernel.fol.FOL.*
 import lisa.kernel.proof.RunningTheory
@@ -9,6 +8,7 @@ import lisa.kernel.proof.SCProof
 import lisa.kernel.proof.SCProofChecker
 import lisa.kernel.proof.SequentCalculus.*
 import org.scalatest.funsuite.AnyFunSuite
+import utilities.KernelHelpers.{_, given}
 
 import scala.collection.immutable.SortedSet
 import scala.util.Random
diff --git a/src/test/scala/lisa/kernel/IncorrectProofsTests.scala b/src/test/scala/lisa/kernel/IncorrectProofsTests.scala
index 213336b64dc14311d269d0dd3d60fa38e85ae10d..840dbd5d3082f434a50fb957b5231781afc2de46 100644
--- a/src/test/scala/lisa/kernel/IncorrectProofsTests.scala
+++ b/src/test/scala/lisa/kernel/IncorrectProofsTests.scala
@@ -1,11 +1,11 @@
 package lisa.kernel
 
 //import lisa.settheory.AxiomaticSetTheory.{emptySet, emptySetAxiom, pair, pairAxiom, useAxiom}
-import utilities.KernelHelpers.*
 import lisa.kernel.fol.FOL.*
 import lisa.kernel.proof.SCProof
 import lisa.kernel.proof.SequentCalculus.*
 import test.ProofCheckerSuite
+import utilities.KernelHelpers.*
 
 import scala.collection.immutable.SortedSet
 import scala.language.implicitConversions
diff --git a/src/test/scala/lisa/kernel/ProofTests.scala b/src/test/scala/lisa/kernel/ProofTests.scala
index b132433709c7dcca2d70a11e90a23b361eb51a59..fc559c9a75105307136b7fd0b6d6620da60589f1 100644
--- a/src/test/scala/lisa/kernel/ProofTests.scala
+++ b/src/test/scala/lisa/kernel/ProofTests.scala
@@ -1,6 +1,5 @@
 package lisa.kernel
 
-import utilities.KernelHelpers.{_, given}
 import lisa.kernel.Printer
 import lisa.kernel.fol.FOL.*
 import lisa.kernel.proof.RunningTheory
@@ -9,6 +8,7 @@ import lisa.kernel.proof.SCProof
 import lisa.kernel.proof.SCProofChecker
 import lisa.kernel.proof.SequentCalculus.*
 import org.scalatest.funsuite.AnyFunSuite
+import utilities.KernelHelpers.{_, given}
 
 import scala.util.Random
 
diff --git a/src/test/scala/lisa/proven/ElementsOfSetTheoryTests.scala b/src/test/scala/lisa/proven/ElementsOfSetTheoryTests.scala
index fde50ed0fa44ab306a93559c5912e1749389057f..b9e09182ecdb26f35689f42134711a4ef1ae6798 100644
--- a/src/test/scala/lisa/proven/ElementsOfSetTheoryTests.scala
+++ b/src/test/scala/lisa/proven/ElementsOfSetTheoryTests.scala
@@ -2,15 +2,16 @@ package proven
 
 import lisa.kernel.Printer
 import lisa.kernel.fol.FOL.*
+import lisa.kernel.fol.FOL.*
 import lisa.kernel.proof.SCProof
 import lisa.kernel.proof.SequentCalculus.Sequent
-import lisa.kernel.fol.FOL.*
-import utilities.KernelHelpers.{*, given}
 import lisa.kernel.proof.SequentCalculus.*
 import lisa.settheory.AxiomaticSetTheory.*
 import proven.ElementsOfSetTheory.*
 import proven.tactics.ProofTactics
 import test.ProofCheckerSuite
+import utilities.KernelHelpers.{_, given}
+import utilities.KernelHelpers.{_, given}
 
 class ElementsOfSetTheoryTests extends ProofCheckerSuite {
 
diff --git a/src/test/scala/lisa/proven/SimpleProverTests.scala b/src/test/scala/lisa/proven/SimpleProverTests.scala
index 05bd4c4ab2614490e20ac5444ac4619c760eb90d..e0b99c734ee9091a7e5daad84562aabfe017f3a3 100644
--- a/src/test/scala/lisa/proven/SimpleProverTests.scala
+++ b/src/test/scala/lisa/proven/SimpleProverTests.scala
@@ -1,6 +1,5 @@
 package proven
 
-import utilities.KernelHelpers.*
 import lisa.kernel.Printer
 import lisa.kernel.Printer.*
 import lisa.kernel.fol.FOL.*
@@ -8,9 +7,10 @@ import lisa.kernel.proof.RunningTheory
 import lisa.kernel.proof.RunningTheory.PredicateLogic
 import lisa.kernel.proof.SCProofChecker
 import org.scalatest.funsuite.AnyFunSuite
-import utilities.tptp.ProblemGatherer.getPRPproblems
-import utilities.tptp.KernelParser.*
 import proven.tactics.SimplePropositionalSolver as SPS
+import utilities.KernelHelpers.*
+import utilities.tptp.KernelParser.*
+import utilities.tptp.ProblemGatherer.getPRPproblems
 
 class SimpleProverTests extends AnyFunSuite {
 
diff --git a/src/test/scala/test/ProofCheckerSuite.scala b/src/test/scala/test/ProofCheckerSuite.scala
index 08d91983ff5457771008de72604cb0208888b9ba..8a6011d729cf0cdd1a0409d4028a9555a82327fe 100644
--- a/src/test/scala/test/ProofCheckerSuite.scala
+++ b/src/test/scala/test/ProofCheckerSuite.scala
@@ -7,7 +7,6 @@ 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 utilities.KernelHelpers._
 import utilities.KernelHelpers.given_Conversion_Boolean_List_String_Option