diff --git a/build.sbt b/build.sbt
index 70c4dbe49303821fbfdc9aac6436a116f57a2995..1699b485af425c1089b7cbb613b8e71738479de1 100644
--- a/build.sbt
+++ b/build.sbt
@@ -4,7 +4,7 @@ licenses := Seq("Apache-2.0" -> url("https://www.apache.org/licenses/LICENSE-2.0
 
 version := "0.1"
 
-scalaVersion := "3.0.2"
+scalaVersion := "3.1.3"
 
 scalacOptions ++= Seq("-deprecation", "-feature")
 scalacOptions ++= Seq(
diff --git a/src/main/scala/dev/A.scala b/src/main/scala/dev/A.scala
new file mode 100644
index 0000000000000000000000000000000000000000..e9ddcd2468061333c9b6cd35398476047a1ceaca
--- /dev/null
+++ b/src/main/scala/dev/A.scala
@@ -0,0 +1,5 @@
+package dev
+
+trait A extends WithMain {}
+
+object A extends A
diff --git a/src/main/scala/dev/WithMain.scala b/src/main/scala/dev/WithMain.scala
new file mode 100644
index 0000000000000000000000000000000000000000..72454a97945a417a6c3f4015040c5dee6ff8037f
--- /dev/null
+++ b/src/main/scala/dev/WithMain.scala
@@ -0,0 +1,8 @@
+package dev
+
+abstract class WithMain {
+  def main(args: Array[String]): Unit = {
+    println("Bonjour")
+  }
+
+}
diff --git a/src/main/scala/lisa/kernel/proof/RunningTheory.scala b/src/main/scala/lisa/kernel/proof/RunningTheory.scala
index 4e1625ff23bb6602754aa4e24186df6efa0feed6..95280f5ec7e38aba4fc1775e5c10b5b3993a6885 100644
--- a/src/main/scala/lisa/kernel/proof/RunningTheory.scala
+++ b/src/main/scala/lisa/kernel/proof/RunningTheory.scala
@@ -29,12 +29,12 @@ class RunningTheory {
   /**
    * A theorem encapsulate a sequent and assert that this sequent has been correctly proven and may be used safely in further proofs.
    */
-  final case class Theorem private[RunningTheory](name: String, proposition: Sequent) extends Justification
+  final case class Theorem private[RunningTheory] (name: String, proposition: Sequent) extends Justification
 
   /**
    * An axiom is any formula that is assumed and considered true within the theory. It can freely be used later in any proof.
    */
-  final case class Axiom private[RunningTheory](name: String, ax: Formula) extends Justification
+  final case class Axiom private[RunningTheory] (name: String, ax: Formula) extends Justification
 
   /**
    * A definition can be either a PredicateDefinition or a FunctionDefinition.
@@ -48,7 +48,7 @@ class RunningTheory {
    * @param args  The variables representing the arguments of the predicate in the formula phi.
    * @param phi   The formula defining the predicate.
    */
-  final case class PredicateDefinition private[RunningTheory](label: ConstantPredicateLabel, args: Seq[VariableLabel], phi: Formula) extends Definition
+  final case class PredicateDefinition private[RunningTheory] (label: ConstantPredicateLabel, args: Seq[VariableLabel], phi: Formula) extends Definition
 
   /**
    * Define a function symbol as the unique element that has some property. The existence and uniqueness
@@ -60,7 +60,7 @@ class RunningTheory {
    * @param out   The variable representing the result of the function in phi
    * @param phi   The formula defining the function.
    */
-  final case class FunctionDefinition private[RunningTheory](label: ConstantFunctionLabel, args: Seq[VariableLabel], out: VariableLabel, phi: Formula) extends Definition
+  final case class FunctionDefinition private[RunningTheory] (label: ConstantFunctionLabel, args: Seq[VariableLabel], out: VariableLabel, phi: Formula) extends Definition
 
   private[proof] val theoryAxioms: mMap[String, Axiom] = mMap.empty
   private[proof] val theorems: mMap[String, Theorem] = mMap.empty
@@ -103,7 +103,7 @@ class RunningTheory {
             val thm = Theorem(name, proof.conclusion)
             theorems.update(name, thm)
             ValidJustification(thm)
-          case r@SCProofCheckerJudgement.SCInvalidProof(_, _, message) =>
+          case r @ SCProofCheckerJudgement.SCInvalidProof(_, _, message) =>
             InvalidJustification("The given proof is incorrect: " + message, Some(r))
         }
       else InvalidJustification("All symbols in the conclusion of the proof must belong to the theory. You need to add missing symbols to the theory.", None)
@@ -147,13 +147,13 @@ class RunningTheory {
    * @return A definition object if the parameters are correct,
    */
   def makeFunctionDefinition(
-                                proof: SCProof,
-                                justifications: Seq[Justification],
-                                label: ConstantFunctionLabel,
-                                args: Seq[VariableLabel],
-                                out: VariableLabel,
-                                phi: Formula
-                            ): RunningTheoryJudgement[this.FunctionDefinition] = {
+      proof: SCProof,
+      justifications: Seq[Justification],
+      label: ConstantFunctionLabel,
+      args: Seq[VariableLabel],
+      out: VariableLabel,
+      phi: Formula
+  ): RunningTheoryJudgement[this.FunctionDefinition] = {
     if (belongsToTheory(phi))
       if (isAvailable(label))
         if (phi.freeVariables.subsetOf(args.toSet + out) && phi.schematicFunctions.isEmpty && phi.schematicPredicates.isEmpty)
@@ -173,7 +173,7 @@ class RunningTheory {
                     } else InvalidJustification("The proof is correct but its conclusion does not correspond to a definition for the formula phi.", None)
                   case _ => InvalidJustification("The conclusion of the proof must have an empty left hand side, and a single formula on the right hand side.", None)
                 }
-              case r@SCProofCheckerJudgement.SCInvalidProof(_, path, message) => InvalidJustification("The given proof is incorrect: " + message, Some(r))
+              case r @ SCProofCheckerJudgement.SCInvalidProof(_, path, message) => InvalidJustification("The given proof is incorrect: " + message, Some(r))
             }
           else InvalidJustification("Not all imports of the proof are correctly justified.", None)
         else InvalidJustification("The definition is not allowed to contain schematic symbols or free variables.", None)
@@ -282,7 +282,7 @@ class RunningTheory {
    */
 
   def addSymbol(s: ConstantLabel): Unit = {
-    if (isAvailable(s)){
+    if (isAvailable(s)) {
       knownSymbols.update(s.id, s)
       s match
         case c: ConstantFunctionLabel => funDefinitions.update(c, None)
diff --git a/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala b/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala
index 0bb0cbc8a3a781d573ecc08194284e2be414ba5e..d4f35c040e1758289fda2d37febeb382493086d0 100644
--- a/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala
+++ b/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala
@@ -8,13 +8,11 @@ import utilities.Helpers.{_, given}
  * Base trait for set theoretical axiom systems.
  * Defines the symbols used in set theory.
  */
-private[settheory] trait SetTheoryDefinitions {
-  type Axiom = Formula
-  def axioms: Set[(String, Axiom)] = Set.empty
-  private[settheory] final val (x, y, z, a, b) =
-    (VariableLabel("x"), VariableLabel("y"), VariableLabel("z"), VariableLabel("A"), VariableLabel("B"))
-  final val sPhi = SchematicPredicateLabel("P", 2)
-  final val sPsi = SchematicPredicateLabel("P", 3)
+trait SetTheoryDefinitions {
+
+  private val tete = "tete"
+  def axioms: Set[(String, Formula)] = Set.empty
+
   // Predicates
   final val in = ConstantPredicateLabel("set_membership", 2)
   final val subset = ConstantPredicateLabel("subset_of", 2)
@@ -33,7 +31,7 @@ private[settheory] trait SetTheoryDefinitions {
   final val functions = Set(emptySet, pair, singleton, powerSet, union, universe)
 
   val runningSetTheory: RunningTheory = new RunningTheory()
-  given RunningTheory = runningSetTheory
+  // given RunningTheory = runningSetTheory
 
   predicates.foreach(s => runningSetTheory.addSymbol(s))
   functions.foreach(s => runningSetTheory.addSymbol(s))
diff --git a/src/main/scala/lisa/settheory/SetTheoryTGAxioms.scala b/src/main/scala/lisa/settheory/SetTheoryTGAxioms.scala
index 81b81922de16ce5817a0add565bcf61d31477fe3..53e837d11ca738fc6b418408d9f9de86f0de0b28 100644
--- a/src/main/scala/lisa/settheory/SetTheoryTGAxioms.scala
+++ b/src/main/scala/lisa/settheory/SetTheoryTGAxioms.scala
@@ -6,9 +6,11 @@ import utilities.Helpers.{_, given}
 /**
  * Axioms for the Tarski-Grothendieck theory (TG)
  */
-private[settheory] trait SetTheoryTGAxioms extends SetTheoryZFAxioms {
+trait SetTheoryTGAxioms extends SetTheoryZFAxioms {
+  private val (x, y, z) =
+    (VariableLabel("x"), VariableLabel("y"), VariableLabel("z"))
 
-  final val tarskiAxiom: Axiom = forall(
+  final val tarskiAxiom: Formula = forall(
     x,
     in(x, universe(x)) /\
       forall(
@@ -20,6 +22,6 @@ private[settheory] trait SetTheoryTGAxioms extends SetTheoryZFAxioms {
 
   runningSetTheory.addAxiom("TarskiAxiom", tarskiAxiom)
 
-  override def axioms: Set[(String, Axiom)] = super.axioms + (("TarskiAxiom", tarskiAxiom))
+  override def axioms: Set[(String, Formula)] = super.axioms + (("TarskiAxiom", tarskiAxiom))
 
 }
diff --git a/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala b/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala
index 11fde4e4eb4e2dd94f99511f88123fd1a7394ed2..3e59d388a95ea5eeff19d435e9fc92634bbca78e 100644
--- a/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala
+++ b/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala
@@ -7,18 +7,22 @@ import utilities.Helpers.{_, given}
 /**
  * Axioms for the Zermelo theory (Z)
  */
-private[settheory] trait SetTheoryZAxioms extends SetTheoryDefinitions {
+trait SetTheoryZAxioms extends SetTheoryDefinitions {
 
-  final val emptySetAxiom: Axiom = forall(x, !in(x, emptySet()))
-  final val extensionalityAxiom: Axiom = forall(x, forall(y, forall(z, in(z, x) <=> in(z, y)) <=> (x === y)))
-  final val pairAxiom: Axiom = forall(x, forall(y, forall(z, in(z, pair(x, y)) <=> (x === z) \/ (y === z))))
-  final val unionAxiom: Axiom = forall(x, forall(z, in(x, union(z)) <=> exists(y, in(x, y) /\ in(y, z))))
-  final val powerAxiom: Axiom = forall(x, forall(y, in(x, powerSet(y)) <=> subset(x, y)))
-  final val foundationAxiom: Axiom = forall(x, !(x === emptySet()) ==> exists(y, in(y, x) /\ forall(z, in(z, x) ==> !in(z, y))))
+  private val (x, y, z) =
+    (VariableLabel("x"), VariableLabel("y"), VariableLabel("z"))
+  private final val sPhi = SchematicPredicateLabel("P", 2)
 
-  final val comprehensionSchema: Axiom = forall(z, exists(y, forall(x, in(x, y) <=> (in(x, z) /\ sPhi(x, z)))))
+  final val emptySetAxiom: Formula = forall(x, !in(x, emptySet()))
+  final val extensionalityAxiom: Formula = forall(x, forall(y, forall(z, in(z, x) <=> in(z, y)) <=> (x === y)))
+  final val pairAxiom: Formula = forall(x, forall(y, forall(z, in(z, pair(x, y)) <=> (x === z) \/ (y === z))))
+  final val unionAxiom: Formula = forall(x, forall(z, in(x, union(z)) <=> exists(y, in(x, y) /\ in(y, z))))
+  final val powerAxiom: Formula = forall(x, forall(y, in(x, powerSet(y)) <=> subset(x, y)))
+  final val foundationAxiom: Formula = forall(x, !(x === emptySet()) ==> exists(y, in(y, x) /\ forall(z, in(z, x) ==> !in(z, y))))
 
-  private val zAxioms: Set[(String, Axiom)] = Set(
+  final val comprehensionSchema: Formula = forall(z, exists(y, forall(x, in(x, y) <=> (in(x, z) /\ sPhi(x, z)))))
+
+  private val zAxioms: Set[(String, Formula)] = Set(
     ("EmptySet", emptySetAxiom),
     ("extensionalityAxiom", extensionalityAxiom),
     ("pairAxiom", pairAxiom),
@@ -30,6 +34,6 @@ private[settheory] trait SetTheoryZAxioms extends SetTheoryDefinitions {
 
   zAxioms.foreach(a => runningSetTheory.addAxiom(a._1, a._2))
 
-  override def axioms: Set[(String, Axiom)] = super.axioms ++ zAxioms
+  override def axioms: Set[(String, Formula)] = super.axioms ++ zAxioms
 
 }
diff --git a/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala b/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala
index e89ea065be30ad3354e1b7bbfa1049f754e52d3e..50eaf462b6eb29d869a0564057c02a614be9fdc4 100644
--- a/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala
+++ b/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala
@@ -6,15 +6,18 @@ import utilities.Helpers.{_, given}
 /**
  * Axioms for the Zermelo-Fraenkel theory (ZF)
  */
-private[settheory] trait SetTheoryZFAxioms extends SetTheoryZAxioms {
+trait SetTheoryZFAxioms extends SetTheoryZAxioms {
+  private val (x, y, a, b) =
+    (VariableLabel("x"), VariableLabel("y"), VariableLabel("A"), VariableLabel("B"))
+  private final val sPsi = SchematicPredicateLabel("P", 3)
 
-  final val replacementSchema: Axiom = forall(
+  final val replacementSchema: Formula = forall(
     a,
     forall(x, (in(x, a)) ==> existsOne(y, sPsi(a, x, y))) ==>
       exists(b, forall(x, in(x, a) ==> exists(y, in(y, b) /\ sPsi(a, x, y))))
   )
   runningSetTheory.addAxiom("replacementSchema", replacementSchema)
 
-  override def axioms: Set[(String, Axiom)] = super.axioms + (("replacementSchema", replacementSchema))
+  override def axioms: Set[(String, Formula)] = super.axioms + (("replacementSchema", replacementSchema))
 
 }
diff --git a/src/main/scala/proven/DSetTheory/Part1.scala b/src/main/scala/proven/DSetTheory/Part1.scala
index 331916cc558db0ac818f310f44a056b95a79cf1f..8b69a2b4f0bd8cee213fe22b59482e6901e44ab4 100644
--- a/src/main/scala/proven/DSetTheory/Part1.scala
+++ b/src/main/scala/proven/DSetTheory/Part1.scala
@@ -19,7 +19,7 @@ import utilities.Printer.prettySequent
 
 import scala.collection.immutable
 import scala.collection.immutable.SortedSet
-object Part1 {
+trait Part1 {
   val theory = AxiomaticSetTheory.runningSetTheory
   def axiom(f: Formula): theory.Axiom = theory.getAxiom(f).get
 
@@ -33,6 +33,9 @@ object Part1 {
   private val g = SchematicFunctionLabel("g", 0)
   private val h = SchematicPredicateLabel("h", 0)
 
+  val sPhi = SchematicPredicateLabel("P", 2)
+  val sPsi = SchematicPredicateLabel("P", 3)
+
   given Conversion[SchematicFunctionLabel, Term] with
     def apply(s: SchematicFunctionLabel): Term = s()
 
@@ -92,6 +95,9 @@ object Part1 {
     val B = VariableLabel("B")
     val B1 = VariableLabel("B1")
     val phi = SchematicPredicateLabel("phi", 2)
+    val sPhi = SchematicPredicateLabel("P", 2)
+    val sPsi = SchematicPredicateLabel("P", 3)
+
     val H = existsOne(x, phi(x, a))
     val H1 = forall(a, in(a, A) ==> H)
     val s0 = hypothesis(H) // () |- existsOne(x, phi(x, a)))
diff --git a/src/main/scala/proven/MainLibrary.scala b/src/main/scala/proven/MainLibrary.scala
new file mode 100644
index 0000000000000000000000000000000000000000..c0c1c45a5334c955c460817569ab69f6d25a7944
--- /dev/null
+++ b/src/main/scala/proven/MainLibrary.scala
@@ -0,0 +1,12 @@
+package proven
+
+import lisa.kernel.proof.RunningTheory
+import lisa.settheory.AxiomaticSetTheory
+import lisa.settheory.SetTheoryTGAxioms
+import utilities.Library
+
+abstract class MainLibrary extends Library(AxiomaticSetTheory.runningSetTheory) with SetTheoryTGAxioms {
+  import AxiomaticSetTheory.*
+  override val output: String => Unit = println
+
+}
diff --git a/src/main/scala/proven/SetTheory.scala b/src/main/scala/proven/SetTheory.scala
new file mode 100644
index 0000000000000000000000000000000000000000..84fae876c44e24aeb03f498eccd9ecbf2536b59f
--- /dev/null
+++ b/src/main/scala/proven/SetTheory.scala
@@ -0,0 +1,31 @@
+package proven
+
+import lisa.kernel.fol.FOL.*
+import lisa.kernel.proof.RunningTheory
+import lisa.kernel.proof.RunningTheoryJudgement
+import lisa.kernel.proof.SCProof
+import lisa.kernel.proof.SequentCalculus.*
+import lisa.settheory.AxiomaticSetTheory
+import lisa.settheory.AxiomaticSetTheory.*
+import utilities.Helpers.{_, given}
+
+trait SetTheory extends MainLibrary {
+  private val x = SchematicFunctionLabel("x", 0)
+  private val y = SchematicFunctionLabel("y", 0)
+  private val z = SchematicFunctionLabel("z", 0)
+  private val x_ = VariableLabel("x")
+  private val y_ = VariableLabel("y")
+  private val z_ = VariableLabel("z")
+
+  THEOREM("russelParadox") of ("∀x. (x ∈ ?y) ↔ ¬(x ∈ x) ⊢") PROOF {
+    val contra = in(y, y) <=> !in(y, y)
+    val s0 = Hypothesis(contra |- contra, contra)
+    val s1 = LeftForall(forall(x_, in(x_, y) <=> !in(x_, x_)) |- contra, 0, in(x_, y) <=> !in(x_, x_), x_, y)
+    val s2 = Rewrite(forall(x_, in(x_, y) <=> !in(x_, x_)) |- (), 1)
+    SCProof(s0, s1, s2)
+  } using ()
+
+  thm"russelParadox".show()
+}
+
+object SetTheory extends SetTheory {}
diff --git a/src/main/scala/utilities/Library.scala b/src/main/scala/utilities/Library.scala
new file mode 100644
index 0000000000000000000000000000000000000000..6f505e44bdf201127f53593be94e9f96760459f7
--- /dev/null
+++ b/src/main/scala/utilities/Library.scala
@@ -0,0 +1,124 @@
+package utilities
+
+import lisa.kernel.proof.RunningTheory
+import lisa.kernel.proof.RunningTheoryJudgement
+import lisa.kernel.proof.SCProof
+
+import Helpers.{given, *}
+
+abstract class Library(val theory: RunningTheory) {
+  val output: String => Unit
+  type Justification = theory.Justification
+  type Theorem = theory.Theorem
+  val Theorem = theory.Theorem
+  type Definition = theory.Definition
+  type Axiom = theory.Axiom
+  val Axiom = theory.Axiom
+  type PredicateDefinition = theory.PredicateDefinition
+  val PredicateDefinition = theory.PredicateDefinition
+  type FunctionDefinition = theory.FunctionDefinition
+  val FunctionDefinition = theory.FunctionDefinition
+  type Judgement[J <: Justification] = RunningTheoryJudgement[J]
+
+  type Proof = SCProof
+  val Proof = SCProof
+  Proof.apply()
+
+  // extension (s:String) def apply():Unit = ()
+
+  def makeTheorem(name: String, statement: String, proof: SCProof, justifications: Seq[theory.Justification]): RunningTheoryJudgement[theory.Theorem] =
+    theory.theorem(name, statement, proof, justifications)
+
+  case class TheoremNameWithStatement(name: String, statement: String) {
+    def PROOF(proof: SCProof): TheoremNameWithProof = TheoremNameWithProof(name, statement, proof)
+  }
+
+  case class TheoremName(name: String) {
+    def of(statement: String): TheoremNameWithStatement = TheoremNameWithStatement(name, statement)
+  }
+
+  def THEOREM(name: String): TheoremName = TheoremName(name)
+
+  case class TheoremNameWithProof(name: String, statement: String, proof: SCProof) {
+    def using(justifications: theory.Justification*): theory.Theorem = theory.theorem(name, statement, proof, justifications) match
+      case RunningTheoryJudgement.ValidJustification(just) => just
+      case wrongJudgement: RunningTheoryJudgement.InvalidJustification[_] => wrongJudgement.showAndGet(output)
+
+    def using(u: Unit): theory.Theorem = using()
+  }
+
+  given Conversion[TheoremNameWithProof, theory.Theorem] = _.using()
+
+  implicit class JsonHelper(val sc: StringContext) {
+
+    def thm(args: Any*): theory.Theorem = getTheorem(sc.parts.mkString(""))
+
+    def ax(args: Any*): theory.Axiom = getAxiom(sc.parts.mkString(""))
+
+    def defi(args: Any*): theory.Definition = getDefinition(sc.parts.mkString(""))
+  }
+
+  def getTheorem(name: String): theory.Theorem =
+    theory.getTheorem(name) match
+      case Some(value) => value
+      case None => throw java.util.NoSuchElementException(s"No theorem with name \"$name\" was found.")
+
+  def getAxiom(name: String): theory.Axiom =
+    theory.getAxiom(name) match
+      case Some(value) => value
+      case None => throw java.util.NoSuchElementException(s"No axiom with name \"$name\" was found.")
+
+  def getDefinition(name: String): theory.Definition =
+    theory.getDefinition(name) match
+      case Some(value) => value
+      case None => throw java.util.NoSuchElementException(s"No definition for symbol \"$name\" was found.")
+
+  given Conversion[String, theory.Justification] = name => theory.getJustification(name).get
+
+  def main(args: Array[String]): Unit = { println("bonjour") }
+  /*
+    val a:String = "a"
+    val b:String = "b"
+    val c:String = "c"
+    val d:String = "d"
+    val e:String = "e"
+    val f:String = "f"
+    val g:String = "g"
+    val h:String = "h"
+    val i:String = "i"
+    val j:String = "j"
+    val k:String = "k"
+    val l:String = "l"
+    val m:String = "m"
+    val n:String = "n"
+    val o:String = "o"
+    val p:String = "p"
+    val q:String = "q"
+    val r:String = "r"
+    val s:String = "s"
+    val t:String = "t"
+    val u:String = "u"
+    val v:String = "v"
+    val w:String = "w"
+    val x:String = "x"
+    val y:String = "y"
+    val z:String = "z"
+
+    case class SchematicFLabel(s:String){
+        def apply(ts:Term*): FunctionTerm = FunctionTerm(SchematicFunctionLabel(s, ts.length), ts)
+        def apply(n:Int): SchematicFunctionLabel = SchematicFunctionLabel(s, n)
+    }
+
+    case class SchematicPLabel(s:String){
+        def apply(fs:Term*): PredicateFormula = PredicateFormula(SchematicPredicateLabel(s, fs.length), fs)
+        def apply(n:Int): SchematicPredicateLabel = SchematicPredicateLabel(s, n)
+    }
+
+    def ?(s:String) = SchematicFLabel(s)
+    def &(s:String) = SchematicPLabel(s)
+
+    given Conversion[String, VariableLabel] = VariableLabel(_)
+    given Conversion[String, VariableTerm] = s => VariableTerm(VariableLabel(s))
+
+   */
+}
diff --git a/src/main/scala/utilities/TheoriesHelpers.scala b/src/main/scala/utilities/TheoriesHelpers.scala
index fdcb6650b775ce1d6603363b98649b7cfcdf796f..0199ba734878331b2f411760864b65b99825fea9 100644
--- a/src/main/scala/utilities/TheoriesHelpers.scala
+++ b/src/main/scala/utilities/TheoriesHelpers.scala
@@ -16,8 +16,8 @@ trait TheoriesHelpers extends KernelHelpers {
       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)
     }
-    
-    def getJustification(name:String) : Option[theory.Justification] = theory.getAxiom(name).orElse(theory.getTheorem(name)).orElse(theory.getDefinition(name))
+
+    def getJustification(name: String): Option[theory.Justification] = theory.getAxiom(name).orElse(theory.getTheorem(name)).orElse(theory.getDefinition(name))
 
   extension (just: RunningTheory#Justification)
     def show(output: String => Unit = println): just.type = {