From 6d3790d580ed39bbe49d79c24bc13daf0f04403f Mon Sep 17 00:00:00 2001
From: SimonGuilloud <sim-guilloud@bluewin.ch>
Date: Sun, 12 Jun 2022 11:58:21 +0200
Subject: [PATCH] Ran scalafmt

---
 src/main/scala/Example.scala                  |  8 +--
 .../lisa/kernel/proof/RunningTheory.scala     |  2 +-
 .../lisa/settheory/SetTheoryDefinitions.scala |  2 +-
 .../lisa/settheory/SetTheoryTGAxioms.scala    |  2 +-
 .../lisa/settheory/SetTheoryZAxioms.scala     |  2 +-
 .../lisa/settheory/SetTheoryZFAxioms.scala    |  2 +-
 src/main/scala/proven/DSetTheory/Part1.scala  | 50 +++++++++++--------
 .../scala/proven/ElementsOfSetTheory.scala    | 28 ++++++-----
 .../scala/proven/tactics/Destructors.scala    |  5 +-
 .../scala/proven/tactics/ProofTactics.scala   |  3 +-
 .../tactics/SimplePropositionalSolver.scala   |  3 +-
 src/main/scala/utilities/KernelHelpers.scala  |  9 ++--
 .../scala/utilities/TheoriesHelpers.scala     | 19 ++++---
 .../scala/utilities/tptp/KernelParser.scala   |  2 +-
 .../lisa/kernel/EquivalenceCheckerTests.scala |  2 +-
 src/test/scala/lisa/kernel/FolTests.scala     |  2 +-
 .../lisa/kernel/IncorrectProofsTests.scala    |  2 +-
 src/test/scala/lisa/kernel/ProofTests.scala   |  2 +-
 .../proven/ElementsOfSetTheoryTests.scala     |  5 +-
 .../scala/lisa/proven/SimpleProverTests.scala |  6 +--
 src/test/scala/test/ProofCheckerSuite.scala   |  1 -
 21 files changed, 84 insertions(+), 73 deletions(-)

diff --git a/src/main/scala/Example.scala b/src/main/scala/Example.scala
index 8e7eb102..49a5bf92 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 49e6e1a0..70f54f3c 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 3f630ed2..cb030de9 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 12fcff5c..6bd499c0 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 da11ebd9..5a47aad9 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 24271f81..13221cc1 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 20e8e8af..3d674ce8 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 e39d29e9..c1fd97c4 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 396c6caa..86fdd967 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 bd90e0a7..50b4d61a 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 87b85b60..a48c558f 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 73650c96..2e7ac736 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 2040ba05..e0f9864e 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 036242c5..3f7d2fe0 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 518ce3f9..2576c9c9 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 615d58e1..7ebe445c 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 213336b6..840dbd5d 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 b1324337..fc559c9a 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 fde50ed0..b9e09182 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 05bd4c4a..e0b99c73 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 08d91983..8a6011d7 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
 
-- 
GitLab