diff --git a/lisa b/lisa
index 7f74dd0..3ae1c20 160000
--- a/lisa
+++ b/lisa
@@ -1 +1 @@
-Subproject commit 7f74dd020d0ec0f245e7587c3b8647ba2357cd63
+Subproject commit 3ae1c204df54e780ab7565070575b421b119f684
diff --git a/project/plugins.sbt b/project/plugins.sbt
new file mode 100644
index 0000000..cb13b37
--- /dev/null
+++ b/project/plugins.sbt
@@ -0,0 +1 @@
+addSbtPlugin("ch.epfl.scala" % "sbt-scalafix" % "0.9.34")
diff --git a/src/main/scala/me/cassayre/florian/masterproject/examples/proofOptimization.scala b/src/main/scala/me/cassayre/florian/masterproject/examples/proofOptimization.scala
index e0abdda..0c3f588 100644
--- a/src/main/scala/me/cassayre/florian/masterproject/examples/proofOptimization.scala
+++ b/src/main/scala/me/cassayre/florian/masterproject/examples/proofOptimization.scala
@@ -1,7 +1,7 @@
 package me.cassayre.florian.masterproject.examples
 
 import lisa.kernel.fol.FOL.*
-import lisa.KernelHelpers.*
+import utilities.Helpers.*
 import lisa.kernel.proof.SequentCalculus.*
 import lisa.kernel.proof.{SCProof, SCProofChecker}
 import me.cassayre.florian.masterproject.front.printer.KernelPrinter
@@ -17,7 +17,7 @@ import me.cassayre.florian.masterproject.util.SCUtils
   def testProofOptimization(proof: SCProof): Unit = {
     val originalChecked = SCProofChecker.checkSCProof(proof)
     println("Original proof:")
-    println(KernelPrinter.prettyProof(proof, judgement = originalChecked))
+    println(KernelPrinter.prettyJudgedProof(originalChecked))
 
     assert(originalChecked.isValid)
 
@@ -25,7 +25,7 @@ import me.cassayre.florian.masterproject.util.SCUtils
     val optimizedChecked = SCProofChecker.checkSCProof(optimized)
     println()
     println("Simplified proof:")
-    println(KernelPrinter.prettyProof(optimized, judgement = optimizedChecked))
+    println(KernelPrinter.prettyJudgedProof(optimizedChecked))
 
     assert(proof.conclusion == optimized.conclusion) // The conclusion must remain the same
     assert(optimizedChecked.isValid) // The proof must still be valid
diff --git a/src/main/scala/me/cassayre/florian/masterproject/front/printer/KernelPrinter.scala b/src/main/scala/me/cassayre/florian/masterproject/front/printer/KernelPrinter.scala
index ec9f601..f1d0196 100644
--- a/src/main/scala/me/cassayre/florian/masterproject/front/printer/KernelPrinter.scala
+++ b/src/main/scala/me/cassayre/florian/masterproject/front/printer/KernelPrinter.scala
@@ -1,5 +1,6 @@
 package me.cassayre.florian.masterproject.front.printer
 
+import lisa.kernel.proof.SCProof
 import lisa.kernel.proof.SCProofCheckerJudgement.*
 import lisa.kernel.proof.{SCProofCheckerJudgement, SequentCalculus as SC}
 import lisa.kernel.fol.FOL
@@ -30,7 +31,11 @@ object KernelPrinter {
     Sequent(sorted(s.left.toIndexedSeq.map(fromKernel)), sorted(s.right.toIndexedSeq.map(fromKernel)))
   }
 
-  def prettyProof(scProof: lisa.kernel.proof.SCProof, style: FrontPrintStyle = FrontPrintStyle.Unicode, compact: Boolean = false, explicit: Boolean = false, judgement: SCProofCheckerJudgement = SCValidProof): String = {
+  def prettyProof(scProof: SCProof, style: FrontPrintStyle = FrontPrintStyle.Unicode, compact: Boolean = false, explicit: Boolean = false): String =
+    prettyJudgedProof(SCValidProof(scProof), style, compact, explicit)
+
+  def prettyJudgedProof(judgement: SCProofCheckerJudgement, style: FrontPrintStyle = FrontPrintStyle.Unicode, compact: Boolean = false, explicit: Boolean = false): String = {
+    val scProof = judgement.proof
     val p = FrontPrintParameters(style, compact)
     val r = KernelRuleIdentifiers(p.s)
     def prettyName(name: String): String = style match {
@@ -162,8 +167,8 @@ object KernelPrinter {
         val fullPath = i +: path
 
         val prefix = judgement match {
-          case SCValidProof => ""
-          case SCInvalidProof(errorPath, _) => if(errorPath.reverse == fullPath) proofStepIndicator else proofStepNoIndicator
+          case SCValidProof(_) => ""
+          case SCInvalidProof(_, errorPath, _) => if(errorPath.reverse == fullPath) proofStepIndicator else proofStepNoIndicator
         }
 
         prefix +
@@ -188,8 +193,8 @@ object KernelPrinter {
     }
 
     val errorSeq = judgement match {
-      case SCValidProof => Seq.empty
-      case SCInvalidProof(path, message) => Seq(s"Proof checker has reported an error at line ${path.mkString(".")}: $message")
+      case SCValidProof(_) => Seq.empty
+      case SCInvalidProof(_, path, message) => Seq(s"Proof checker has reported an error at line ${path.mkString(".")}: $message")
     }
 
     val allLinesPairs = recursivePrint(proof, Seq.empty)
diff --git a/src/main/scala/me/cassayre/florian/masterproject/front/proof/sequent/SequentDefinitions.scala b/src/main/scala/me/cassayre/florian/masterproject/front/proof/sequent/SequentDefinitions.scala
index 15b3a0e..57e7a90 100644
--- a/src/main/scala/me/cassayre/florian/masterproject/front/proof/sequent/SequentDefinitions.scala
+++ b/src/main/scala/me/cassayre/florian/masterproject/front/proof/sequent/SequentDefinitions.scala
@@ -1,6 +1,6 @@
 package me.cassayre.florian.masterproject.front.proof.sequent
 
-import lisa.kernel.Printer
+import utilities.Printer
 import me.cassayre.florian.masterproject.front.fol.FOL.*
 
 trait SequentDefinitions {
diff --git a/src/main/scala/me/cassayre/florian/masterproject/front/proof/state/ProofEnvironmentDefinitions.scala b/src/main/scala/me/cassayre/florian/masterproject/front/proof/state/ProofEnvironmentDefinitions.scala
index 8120235..772327a 100644
--- a/src/main/scala/me/cassayre/florian/masterproject/front/proof/state/ProofEnvironmentDefinitions.scala
+++ b/src/main/scala/me/cassayre/florian/masterproject/front/proof/state/ProofEnvironmentDefinitions.scala
@@ -1,6 +1,6 @@
 package me.cassayre.florian.masterproject.front.proof.state
 
-import lisa.kernel.Printer
+import utilities.Printer
 import lisa.kernel.proof.{RunningTheory, SCProof, SCProofChecker}
 import lisa.kernel.proof.RunningTheoryJudgement.*
 import lisa.kernel.proof.SequentCalculus.{SCSubproof, sequentToFormula}
@@ -31,8 +31,8 @@ trait ProofEnvironmentDefinitions extends ProofStateDefinitions {
 
     override def contains(sequent: Sequent): Boolean = proven.contains(sequent)
 
-    def belongsToTheory(label: ConstantFunctionLabel[?]): Boolean = runningTheory.isAcceptedFunctionLabel(toKernel(label))
-    def belongsToTheory(label: ConstantPredicateLabel[?]): Boolean = runningTheory.isAcceptedPredicateLabel(toKernel(label))
+    def belongsToTheory(label: ConstantFunctionLabel[?]): Boolean = runningTheory.isSymbol(toKernel(label))
+    def belongsToTheory(label: ConstantPredicateLabel[?]): Boolean = runningTheory.isSymbol(toKernel(label))
     def belongsToTheory(term: Term): Boolean =
       functionsOf(term).collect { case f: ConstantFunctionLabel[?] => f }.forall(belongsToTheory)
     def belongsToTheory(formula: Formula): Boolean =
@@ -53,7 +53,7 @@ trait ProofEnvironmentDefinitions extends ProofStateDefinitions {
           Seq(
             "Error: the theorem was found to produce an invalid proof; this could indicate a problem with a tactic or a bug in the implementation",
             "The produced proof is shown below for reference:",
-            Printer.prettySCProof(scProof, judgement)
+            Printer.prettySCProof(judgement)
           ).mkString("\n")
         )
       }
@@ -62,7 +62,7 @@ trait ProofEnvironmentDefinitions extends ProofStateDefinitions {
       val justifications = justificationPairs.map { case (justification, _) => justification }
 
       val kernelJustifications = justificationPairs.map { case (_, kernelJustification) => kernelJustification }
-      val kernelTheorem = runningTheory.proofToTheorem(s"t${proven.size}", scProof, kernelJustifications) match {
+      val kernelTheorem = runningTheory.makeTheorem(s"t${proven.size}", scProof.conclusion, scProof, kernelJustifications) match {
         case ValidJustification(result) => result
         case InvalidJustification(_, _) => throw new Error // Should have been caught before
       }
@@ -169,7 +169,7 @@ trait ProofEnvironmentDefinitions extends ProofStateDefinitions {
         Seq(
           "Error: the reconstructed proof was found to be invalid; this could indicate a bug in the implementation of this very method",
           "The reconstructed proof is shown below for reference:",
-          Printer.prettySCProof(scProof, judgement)
+          Printer.prettySCProof(judgement)
         ).mkString("\n")
       )
     }
diff --git a/src/main/scala/me/cassayre/florian/masterproject/legacy/GoalBasedProofSystem.scala b/src/main/scala/me/cassayre/florian/masterproject/legacy/GoalBasedProofSystem.scala
index 6e2cf8a..659a5f0 100644
--- a/src/main/scala/me/cassayre/florian/masterproject/legacy/GoalBasedProofSystem.scala
+++ b/src/main/scala/me/cassayre/florian/masterproject/legacy/GoalBasedProofSystem.scala
@@ -1,9 +1,9 @@
 package me.cassayre.florian.masterproject.legacy
 
 import lisa.kernel.fol.FOL.*
-import lisa.KernelHelpers.*
-import lisa.kernel.Printer
-import lisa.kernel.Printer.*
+import utilities.Helpers.*
+import utilities.Printer
+import utilities.Printer.*
 import lisa.kernel.proof.SequentCalculus.{Hypothesis, Sequent, Weakening, sequentToFormula}
 import lisa.kernel.proof.{RunningTheory, SCProof, SCProofChecker}
 import lisa.settheory.AxiomaticSetTheory
diff --git a/src/main/scala/me/cassayre/florian/masterproject/legacy/GoalBasedProofSystemREPL.scala b/src/main/scala/me/cassayre/florian/masterproject/legacy/GoalBasedProofSystemREPL.scala
index fe06d8b..cec4e10 100644
--- a/src/main/scala/me/cassayre/florian/masterproject/legacy/GoalBasedProofSystemREPL.scala
+++ b/src/main/scala/me/cassayre/florian/masterproject/legacy/GoalBasedProofSystemREPL.scala
@@ -6,7 +6,7 @@ import me.cassayre.florian.masterproject.legacy.GoalBasedProofSystem.*
 import java.util.Scanner
 import scala.util.{Failure, Success, Try}
 import lisa.kernel.fol.FOL.*
-import lisa.kernel.Printer
+import utilities.Printer
 import lisa.kernel.proof.{RunningTheory, SCProofChecker}
 import lisa.settheory.AxiomaticSetTheory
 
@@ -126,7 +126,7 @@ object GoalBasedProofSystemREPL {
                             .println(prettyFrame(prettyProofState(newState.proofState)))
                             .println()
                             .println("All goals have been proven, the proof will now be reconstructed below:")
-                            .println(Printer.prettySCProof(proof, judgement))
+                            .println(Printer.prettySCProof(judgement))
                             .println()
                             .println(
                               if(judgement.isValid)
diff --git a/src/main/scala/me/cassayre/florian/masterproject/legacy/meta/Meta.scala b/src/main/scala/me/cassayre/florian/masterproject/legacy/meta/Meta.scala
index aa25990..7a84c88 100644
--- a/src/main/scala/me/cassayre/florian/masterproject/legacy/meta/Meta.scala
+++ b/src/main/scala/me/cassayre/florian/masterproject/legacy/meta/Meta.scala
@@ -1,6 +1,6 @@
 package me.cassayre.florian.masterproject.legacy.meta
 
-import lisa.kernel.Printer
+import utilities.Printer
 import lisa.kernel.proof.{SCProof, SCProofChecker, SequentCalculus}
 import me.cassayre.florian.masterproject.front.fol.FOL.*
 import me.cassayre.florian.masterproject.legacy.parser.SCReader.*
diff --git a/src/main/scala/me/cassayre/florian/masterproject/legacy/parser/SCResolver.scala b/src/main/scala/me/cassayre/florian/masterproject/legacy/parser/SCResolver.scala
index 5ec1b24..6c53be1 100644
--- a/src/main/scala/me/cassayre/florian/masterproject/legacy/parser/SCResolver.scala
+++ b/src/main/scala/me/cassayre/florian/masterproject/legacy/parser/SCResolver.scala
@@ -1,6 +1,6 @@
 package me.cassayre.florian.masterproject.legacy.parser
 
-import lisa.kernel.Printer
+import utilities.Printer
 import me.cassayre.florian.masterproject.legacy.parser.SCParsed.*
 import lisa.kernel.fol.FOL.*
 import lisa.kernel.proof.SCProof
diff --git a/src/main/scala/me/cassayre/florian/masterproject/legacy/test/front/demo.scala b/src/main/scala/me/cassayre/florian/masterproject/legacy/test/front/demo.scala
index f1e27eb..f192e5e 100644
--- a/src/main/scala/me/cassayre/florian/masterproject/legacy/test/front/demo.scala
+++ b/src/main/scala/me/cassayre/florian/masterproject/legacy/test/front/demo.scala
@@ -1,6 +1,6 @@
 package me.cassayre.florian.masterproject.legacy.test.front
 
-import lisa.kernel.Printer
+import utilities.Printer
 
 import scala.util.chaining.*
 import me.cassayre.florian.masterproject.front.{*, given}
diff --git a/src/main/scala/me/cassayre/florian/masterproject/legacy/test/front/tests.scala b/src/main/scala/me/cassayre/florian/masterproject/legacy/test/front/tests.scala
index 3da4440..f8fd414 100644
--- a/src/main/scala/me/cassayre/florian/masterproject/legacy/test/front/tests.scala
+++ b/src/main/scala/me/cassayre/florian/masterproject/legacy/test/front/tests.scala
@@ -1,7 +1,7 @@
 package me.cassayre.florian.masterproject.legacy.test.front
 
 import me.cassayre.florian.masterproject.front.{*, given}
-import lisa.kernel.Printer
+import utilities.Printer
 import lisa.kernel.proof.SCProofChecker
 
 @main def tests(): Unit = {
@@ -37,7 +37,7 @@ import lisa.kernel.proof.SCProofChecker
     case Some((proof, theorems)) =>
       val judgement = SCProofChecker.checkSCProof(proof)
 
-      println(Printer.prettySCProof(proof, judgement))
+      println(Printer.prettySCProof(judgement))
 
       println()
       if(theorems.nonEmpty) {
diff --git a/src/main/scala/me/cassayre/florian/masterproject/legacy/test/front/tests2.scala b/src/main/scala/me/cassayre/florian/masterproject/legacy/test/front/tests2.scala
index d4bc4ec..e3af575 100644
--- a/src/main/scala/me/cassayre/florian/masterproject/legacy/test/front/tests2.scala
+++ b/src/main/scala/me/cassayre/florian/masterproject/legacy/test/front/tests2.scala
@@ -1,6 +1,6 @@
 package me.cassayre.florian.masterproject.legacy.test.front
 
-import lisa.kernel.Printer
+import utilities.Printer
 import lisa.kernel.proof.SCProofChecker
 import me.cassayre.florian.masterproject.front.{*, given}
 
diff --git a/src/main/scala/me/cassayre/florian/masterproject/legacy/test/front/tests4.scala b/src/main/scala/me/cassayre/florian/masterproject/legacy/test/front/tests4.scala
index b50fe8c..e4e1909 100644
--- a/src/main/scala/me/cassayre/florian/masterproject/legacy/test/front/tests4.scala
+++ b/src/main/scala/me/cassayre/florian/masterproject/legacy/test/front/tests4.scala
@@ -1,6 +1,6 @@
 package me.cassayre.florian.masterproject.legacy.test.front
 
-import lisa.kernel.Printer
+import utilities.Printer
 import lisa.kernel.proof.SCProofChecker
 import me.cassayre.florian.masterproject.front.{*, given}
 import me.cassayre.florian.masterproject.front.theory.SetTheory.*
diff --git a/src/main/scala/me/cassayre/florian/masterproject/legacy/test/front/tests5.scala b/src/main/scala/me/cassayre/florian/masterproject/legacy/test/front/tests5.scala
index 738d110..f40465c 100644
--- a/src/main/scala/me/cassayre/florian/masterproject/legacy/test/front/tests5.scala
+++ b/src/main/scala/me/cassayre/florian/masterproject/legacy/test/front/tests5.scala
@@ -1,6 +1,6 @@
 package me.cassayre.florian.masterproject.legacy.test.front
 
-import lisa.kernel.Printer
+import utilities.Printer
 import me.cassayre.florian.masterproject.front.{*, given}
 import me.cassayre.florian.masterproject.front.theory.SetTheory.*
 
diff --git a/src/main/scala/me/cassayre/florian/masterproject/legacy/test/front/tests6.scala b/src/main/scala/me/cassayre/florian/masterproject/legacy/test/front/tests6.scala
index d42a45f..1bb3df1 100644
--- a/src/main/scala/me/cassayre/florian/masterproject/legacy/test/front/tests6.scala
+++ b/src/main/scala/me/cassayre/florian/masterproject/legacy/test/front/tests6.scala
@@ -1,6 +1,6 @@
 package me.cassayre.florian.masterproject.legacy.test.front
 
-import lisa.kernel.Printer
+import utilities.Printer
 
 import scala.util.chaining.*
 import me.cassayre.florian.masterproject.front.fol.FOL.{*, given}
diff --git a/src/main/scala/me/cassayre/florian/masterproject/legacy/test/front/tmp.scala.old b/src/main/scala/me/cassayre/florian/masterproject/legacy/test/front/tmp.scala.old
new file mode 100644
index 0000000..1d98363
--- /dev/null
+++ b/src/main/scala/me/cassayre/florian/masterproject/legacy/test/front/tmp.scala.old
@@ -0,0 +1,103 @@
+package me.cassayre.florian.masterproject.legacy.test.front
+
+import lisa.kernel.Printer
+
+import scala.util.chaining.*
+import me.cassayre.florian.masterproject.front.{*, given}
+
+@main def tmp(): Unit = {}
+/*val (a, b, c) = (SchematicPredicateLabel[0]("a"), SchematicPredicateLabel[0]("b"), SchematicPredicateLabel[0]("c"))
+
+@main def tmp(): Unit = {
+  import me.cassayre.florian.masterproject.front.theory.SetTheory.*
+
+  val (s, t, u) = (SchematicFunctionLabel[0]("s"), SchematicFunctionLabel[0]("t"), SchematicFunctionLabel[0]("u"))
+  val (x, y, z) = (VariableLabel("x"), VariableLabel("y"), VariableLabel("z"))
+
+  given ProofEnvironment = newSetTheoryEnvironment()
+
+  val axExt: Axiom = axiomExtensionality.asJustified.display()
+  val axEmpty: Axiom = axiomEmpty.asJustified.display()
+  val axUnion: Axiom = axiomUnion.asJustified.display()
+
+  // 1. Generalize universal quantifiers
+
+  val thmExtSchema: Theorem = {
+    val t0 = elimRForallS(
+      RuleParameters()
+        .withPredicate(Notations.p, x => forall(y, forall(z, (z in x) <=> (z in y)) <=> (x === y)))
+        .withFunction(Notations.t, s())
+    )(axExt).get
+
+    val t1 = elimRForallS(
+      RuleParameters()
+        .withPredicate(Notations.p, y => forall(z, (z in s) <=> (z in y)) <=> (s === y))
+        .withFunction(Notations.t, t())
+    )(t0).get
+
+    t1
+  }.display()
+
+  val thmEmptySchema: Theorem = elimRForallS(
+    RuleParameters()
+      .withPredicate(Notations.p, x => !(x in emptySet))
+      .withFunction(Notations.t, s())
+  )(axEmpty).get.display()
+
+  val thmUnionSchema: Theorem = {
+    val t0 = elimRForallS(
+      RuleParameters()
+        .withPredicate(Notations.p, x => forall(z, (x in unionSet(z)) <=> exists(y, (x in y) /\ (y in z))))
+        .withFunction(Notations.t, s())
+    )(axUnion).get
+    val t1 = elimRForallS(
+      RuleParameters()
+        .withPredicate(Notations.p, z => (s in unionSet(z)) <=> exists(y, (s in y) /\ (y in z)))
+        .withFunction(Notations.t, t())
+    )(t0).get
+    t1
+  }.display()
+
+  val _ = {
+    val p = ProofMode(() |- unionSet(emptySet) === emptySet)
+    import p.*
+
+    apply(elimRSubstIff(
+      RuleParameters()
+        .withConnector(Notations.f, identity)
+        .withPredicate(Notations.a, formula"forall z. (z in U({})) <=> (z in {})")
+    ))
+
+    focus(1)
+    val _ = thmExtSchema(Notations.s, unionSet(emptySet))(Notations.t, emptySet)
+
+    apply(justification) // Uses the previously proved theorem
+
+    apply(introRForallS(
+      RuleParameters()
+        .withPredicate(Notations.p, z => formula"\ $z. ($z in U({})) <=> ($z in {})")
+        .withFunction(Notations.t, s())
+    ))
+
+    apply(RuleSubstituteRightIff(
+      RuleParameters()
+        .withConnector(Notations.f, x => x <=> (s in emptySet))
+        .withPredicate(Notations.a, formula"exists y. (?s in y) /\ (y in {})")
+    ))
+
+    focus(1)
+    val _ = thmUnionSchema(t, emptySet).rewrite(state.goals.head).get.display()
+    apply(justification)
+
+    apply(introRIff)
+    apply(introRImp)
+    apply(introLExists(
+      RuleParameters()
+        .withPredicate(Notations.p, y => (s in y) /\ (y in emptySet))
+    ))
+
+    apply(introLAnd)
+
+  }
+
+}*/
diff --git a/src/main/scala/me/cassayre/florian/masterproject/legacy/test/tests.scala b/src/main/scala/me/cassayre/florian/masterproject/legacy/test/tests.scala
index a7fad44..aa3a1b0 100644
--- a/src/main/scala/me/cassayre/florian/masterproject/legacy/test/tests.scala
+++ b/src/main/scala/me/cassayre/florian/masterproject/legacy/test/tests.scala
@@ -1,9 +1,9 @@
 package me.cassayre.florian.masterproject.legacy.test
 
 import lisa.kernel.fol.FOL.*
-import lisa.KernelHelpers.*
+import utilities.Helpers.*
 import me.cassayre.florian.masterproject.legacy.GoalBasedProofSystem.*
-import lisa.kernel.Printer
+import utilities.Printer
 import lisa.kernel.proof.SCProofChecker
 import lisa.settheory.AxiomaticSetTheory
 
diff --git a/src/main/scala/me/cassayre/florian/masterproject/legacy/unification/Unifier.scala b/src/main/scala/me/cassayre/florian/masterproject/legacy/unification/Unifier.scala
index 9c3af82..3d126e4 100644
--- a/src/main/scala/me/cassayre/florian/masterproject/legacy/unification/Unifier.scala
+++ b/src/main/scala/me/cassayre/florian/masterproject/legacy/unification/Unifier.scala
@@ -1,6 +1,6 @@
 package me.cassayre.florian.masterproject.legacy.unification
 
-import lisa.kernel.Printer
+import utilities.Printer
 import me.cassayre.florian.masterproject.front.fol.FOL.*
 
 import scala.annotation.tailrec
diff --git a/src/main/scala/me/cassayre/florian/masterproject/util/MonadicSCProofBuilder.scala b/src/main/scala/me/cassayre/florian/masterproject/util/MonadicSCProofBuilder.scala
index 6178b7b..e54a431 100644
--- a/src/main/scala/me/cassayre/florian/masterproject/util/MonadicSCProofBuilder.scala
+++ b/src/main/scala/me/cassayre/florian/masterproject/util/MonadicSCProofBuilder.scala
@@ -1,7 +1,7 @@
 package me.cassayre.florian.masterproject.util
 
 import lisa.kernel.fol.FOL.*
-import lisa.KernelHelpers.*
+import utilities.Helpers.*
 import lisa.kernel.proof.SCProof
 import lisa.kernel.proof.SequentCalculus.*
 import me.cassayre.florian.masterproject.util.SCProofBuilder.{*, given}
diff --git a/src/main/scala/me/cassayre/florian/masterproject/util/SCProofBuilder.scala b/src/main/scala/me/cassayre/florian/masterproject/util/SCProofBuilder.scala
index 154303e..2e33100 100644
--- a/src/main/scala/me/cassayre/florian/masterproject/util/SCProofBuilder.scala
+++ b/src/main/scala/me/cassayre/florian/masterproject/util/SCProofBuilder.scala
@@ -1,8 +1,8 @@
 package me.cassayre.florian.masterproject.util
 
+import lisa.kernel.fol.FOL
 import lisa.kernel.proof.{SCProof, SequentCalculus}
 import lisa.kernel.proof.SequentCalculus.*
-import lisa.settheory.AxiomaticSetTheory.Axiom
 
 /**
  * The proof builder API, a helper to build kernel proofs.
@@ -38,7 +38,7 @@ object SCProofBuilder {
     infix def by(premises: Int*): SCImplicitProofStep = SCImplicitProofStep(s, premises, Seq.empty)
     infix def by(step: SCProofStep): SCExplicitProofStep = SCExplicitProofStep(step)
     infix def justifiedBy(sequents: Sequent*): SCImplicitProofStep = SCImplicitProofStep(s, Seq.empty, sequents)
-    infix def justifiedBy(axiom: Axiom): SCImplicitProofStep = SCImplicitProofStep(s, Seq.empty, Seq(Sequent(Set.empty, Set(axiom))))
+    infix def justifiedBy(axiom: FOL.Formula): SCImplicitProofStep = SCImplicitProofStep(s, Seq.empty, Seq(Sequent(Set.empty, Set(axiom))))
     def justified: SCImplicitProofStep = SCImplicitProofStep(s, Seq.empty, Seq(s))
   }
 
diff --git a/src/main/scala/me/cassayre/florian/masterproject/util/SCProofStepFinder.scala b/src/main/scala/me/cassayre/florian/masterproject/util/SCProofStepFinder.scala
index ffe0d93..96899cc 100644
--- a/src/main/scala/me/cassayre/florian/masterproject/util/SCProofStepFinder.scala
+++ b/src/main/scala/me/cassayre/florian/masterproject/util/SCProofStepFinder.scala
@@ -3,7 +3,7 @@ package me.cassayre.florian.masterproject.util
 import lisa.kernel.fol.FOL.*
 import lisa.kernel.proof.SequentCalculus.*
 import lisa.kernel.proof.{SCProof, SCProofChecker}
-import lisa.kernel.Printer
+import utilities.Printer
 
 import scala.collection.View
 
diff --git a/src/main/scala/me/cassayre/florian/masterproject/util/SCUtils.scala b/src/main/scala/me/cassayre/florian/masterproject/util/SCUtils.scala
index 54deb53..6f6d9c3 100644
--- a/src/main/scala/me/cassayre/florian/masterproject/util/SCUtils.scala
+++ b/src/main/scala/me/cassayre/florian/masterproject/util/SCUtils.scala
@@ -1,6 +1,6 @@
 package me.cassayre.florian.masterproject.util
 
-import lisa.kernel.Printer
+import utilities.Printer
 import lisa.kernel.fol.FOL.*
 import lisa.kernel.proof.SequentCalculus.*
 import lisa.kernel.proof.SCProof
diff --git a/src/test/scala/me/cassayre/florian/masterproject/front/ProofTests.scala b/src/test/scala/me/cassayre/florian/masterproject/front/ProofTests.scala
index da9f973..8a03222 100644
--- a/src/test/scala/me/cassayre/florian/masterproject/front/ProofTests.scala
+++ b/src/test/scala/me/cassayre/florian/masterproject/front/ProofTests.scala
@@ -6,7 +6,7 @@ import org.scalatest.funsuite.AnyFunSuite
 import me.cassayre.florian.masterproject.front.fol.FOL.*
 import me.cassayre.florian.masterproject.front.proof.Proof.*
 import lisa.kernel.proof.SCProofChecker
-import lisa.kernel.Printer
+import utilities.Printer
 
 class ProofTests extends AnyFunSuite {
 
@@ -21,7 +21,7 @@ class ProofTests extends AnyFunSuite {
       assert(result.nonEmpty)
       val scProof = result.get._1
       val judgement = SCProofChecker.checkSCProof(scProof)
-      println(Printer.prettySCProof(scProof, judgement))
+      println(Printer.prettySCProof(judgement))
       println()
       assert(judgement.isValid)
       assert(scProof.imports.isEmpty)
diff --git a/src/test/scala/me/cassayre/florian/masterproject/legacy/GoalBasedProofSystemTests.scala b/src/test/scala/me/cassayre/florian/masterproject/legacy/GoalBasedProofSystemTests.scala
index eb329ac..1fe8444 100644
--- a/src/test/scala/me/cassayre/florian/masterproject/legacy/GoalBasedProofSystemTests.scala
+++ b/src/test/scala/me/cassayre/florian/masterproject/legacy/GoalBasedProofSystemTests.scala
@@ -3,8 +3,8 @@ package me.cassayre.florian.masterproject.legacy
 import scala.language.adhocExtensions
 
 import lisa.kernel.fol.FOL.*
-import lisa.KernelHelpers.*
-import lisa.kernel.Printer
+import utilities.Helpers.*
+import utilities.Printer
 import lisa.kernel.proof.{RunningTheory, SCProofChecker}
 import lisa.settheory.AxiomaticSetTheory
 import me.cassayre.florian.masterproject.legacy.GoalBasedProofSystem.*
@@ -33,7 +33,7 @@ class GoalBasedProofSystemTests extends AnyFunSuite {
     val judgement = SCProofChecker.checkSCProof(proof)
 
     // For some output
-    println(Printer.prettySCProof(proof, judgement))
+    println(Printer.prettySCProof(judgement))
     println()
 
     assert(judgement.isValid, "The validity of the reconstructed proof couldn't be certified")
diff --git a/src/test/scala/me/cassayre/florian/masterproject/legacy/parser/SCReaderTests.scala b/src/test/scala/me/cassayre/florian/masterproject/legacy/parser/SCReaderTests.scala
index 210fe27..f7b353a 100644
--- a/src/test/scala/me/cassayre/florian/masterproject/legacy/parser/SCReaderTests.scala
+++ b/src/test/scala/me/cassayre/florian/masterproject/legacy/parser/SCReaderTests.scala
@@ -2,7 +2,7 @@ package me.cassayre.florian.masterproject.legacy.parser
 
 import scala.language.adhocExtensions
 
-import lisa.kernel.Printer
+import utilities.Printer
 import lisa.kernel.proof.SCProofChecker
 import org.scalatest.funsuite.AnyFunSuite
 
diff --git a/src/test/scala/me/cassayre/florian/masterproject/util/MonadicSCProofBuilderTests.scala b/src/test/scala/me/cassayre/florian/masterproject/util/MonadicSCProofBuilderTests.scala
index b4c69f0..3b24da6 100644
--- a/src/test/scala/me/cassayre/florian/masterproject/util/MonadicSCProofBuilderTests.scala
+++ b/src/test/scala/me/cassayre/florian/masterproject/util/MonadicSCProofBuilderTests.scala
@@ -2,8 +2,8 @@ package me.cassayre.florian.masterproject.util
 
 import scala.language.adhocExtensions
 
-import lisa.KernelHelpers.*
-import lisa.kernel.Printer
+import utilities.Helpers.*
+import utilities.Printer
 import lisa.kernel.fol.FOL.*
 import lisa.kernel.proof.*
 import lisa.kernel.proof.SequentCalculus.*
diff --git a/src/test/scala/me/cassayre/florian/masterproject/util/SCProofStepFinderTests.scala b/src/test/scala/me/cassayre/florian/masterproject/util/SCProofStepFinderTests.scala
index 1bf6c1e..9706276 100644
--- a/src/test/scala/me/cassayre/florian/masterproject/util/SCProofStepFinderTests.scala
+++ b/src/test/scala/me/cassayre/florian/masterproject/util/SCProofStepFinderTests.scala
@@ -2,8 +2,8 @@ package me.cassayre.florian.masterproject.util
 
 import scala.language.adhocExtensions
 
-import lisa.KernelHelpers.*
-import lisa.kernel.Printer
+import utilities.Helpers.*
+import utilities.Printer
 import lisa.kernel.fol.FOL.*
 import lisa.kernel.proof.*
 import lisa.kernel.proof.SequentCalculus.*
@@ -166,7 +166,7 @@ class SCProofStepFinderTests extends AnyFunSuite {
       Try(proofBuilder.build) match {
         case Success(proof) =>
           SCProofChecker.checkSCProof(proof) match {
-            case SCValidProof => // OK
+            case SCValidProof(_) => // OK
               println(testname)
               println(Printer.prettySCProof(proof))
               println()
@@ -178,7 +178,7 @@ class SCProofStepFinderTests extends AnyFunSuite {
                   assert(view.exists(filter), s"The proof step finder was not able to find the step '$testname'")
                 case SCExplicitProofStep(step) => assert(false)
               }
-            case invalid: SCInvalidProof => throw new AssertionError(s"The reconstructed proof for '$testname' is incorrect:\n${Printer.prettySCProof(proof, invalid)}")
+            case invalid: SCInvalidProof => throw new AssertionError(s"The reconstructed proof for '$testname' is incorrect:\n${Printer.prettySCProof(invalid)}")
           }
         case Failure(exception) => throw new AssertionError(s"Couldn't reconstruct the proof for '$testname'", exception) // Couldn't reconstruct this proof
       }