From 3c5d04181a277270a4174b11ef2f02192950df41 Mon Sep 17 00:00:00 2001
From: SimonGuilloud <sim-guilloud@bluewin.ch>
Date: Mon, 13 Jun 2022 17:53:57 +0200
Subject: [PATCH] Code reorganization and helpers Printer file moved to
 utilities New organisation of helpers, new helper file for RunningTheory and
 their elements. Can show Justifications SCProofCheckerJudgement now contain
 the proof they refer to, no need to pass it explicitely along anymore. Other
 small changes.

---
 src/main/scala/Example.scala                  |   8 +-
 src/main/scala/lisa/kernel/Printer.scala      | 333 ------------------
 .../scala/lisa/kernel/proof/Judgement.scala   |   7 +-
 .../lisa/kernel/proof/RunningTheory.scala     |  71 ++--
 .../lisa/kernel/proof/SCProofChecker.scala    | 221 ++++++------
 .../lisa/settheory/SetTheoryDefinitions.scala |   2 +-
 .../lisa/settheory/SetTheoryTGAxioms.scala    |   3 +-
 .../lisa/settheory/SetTheoryZAxioms.scala     |   2 +-
 .../lisa/settheory/SetTheoryZFAxioms.scala    |   2 +-
 src/main/scala/proven/DSetTheory/Part1.scala  |  22 +-
 .../scala/proven/ElementsOfSetTheory.scala    |  32 +-
 .../scala/proven/tactics/Destructors.scala    |   2 +-
 .../scala/proven/tactics/ProofTactics.scala   |   4 +-
 .../tactics/SimplePropositionalSolver.scala   |   2 +-
 src/main/scala/utilities/KernelHelpers.scala  |   2 +-
 .../scala/utilities/TheoriesHelpers.scala     |  46 ++-
 .../scala/utilities/tptp/KernelParser.scala   |   2 +-
 .../lisa/kernel/EquivalenceCheckerTests.scala |   4 +-
 src/test/scala/lisa/kernel/FolTests.scala     |   4 +-
 .../lisa/kernel/IncorrectProofsTests.scala    |   2 +-
 src/test/scala/lisa/kernel/PrinterTest.scala  |   2 +-
 src/test/scala/lisa/kernel/ProofTests.scala   |   4 +-
 .../proven/ElementsOfSetTheoryTests.scala     |   8 +-
 .../scala/lisa/proven/SimpleProverTests.scala |   8 +-
 src/test/scala/test/ProofCheckerSuite.scala   |  12 +-
 25 files changed, 262 insertions(+), 543 deletions(-)
 delete mode 100644 src/main/scala/lisa/kernel/Printer.scala

diff --git a/src/main/scala/Example.scala b/src/main/scala/Example.scala
index 49a5bf92..a207d70a 100644
--- a/src/main/scala/Example.scala
+++ b/src/main/scala/Example.scala
@@ -1,11 +1,11 @@
-import lisa.kernel.Printer.*
 import lisa.kernel.fol.FOL.*
 import lisa.kernel.proof.SCProof
 import lisa.kernel.proof.SCProofChecker
 import lisa.kernel.proof.SCProofChecker.*
 import lisa.kernel.proof.SequentCalculus.*
 import proven.tactics.SimplePropositionalSolver.solveSequent
-import utilities.KernelHelpers.{_, given}
+import utilities.Helpers.{_, given}
+import utilities.Printer.*
 import utilities.tptp.KernelParser.*
 import utilities.tptp.ProblemGatherer.*
 import utilities.tptp.*
@@ -140,10 +140,6 @@ object Example {
     println("SPC: " + p.spc.mkString(", "))
     p.formulas.foreach(printAnnotatedFormula)
   }
-  private def checkProof(proof: SCProof): Unit = {
-    val error = SCProofChecker.checkSCProof(proof)
-    println(prettySCProof(proof, error))
-  }
 
   val P = SchematicPredicateLabel("P", 1)
 
diff --git a/src/main/scala/lisa/kernel/Printer.scala b/src/main/scala/lisa/kernel/Printer.scala
deleted file mode 100644
index 044c181a..00000000
--- a/src/main/scala/lisa/kernel/Printer.scala
+++ /dev/null
@@ -1,333 +0,0 @@
-package lisa.kernel
-
-import lisa.kernel.fol.FOL.*
-import lisa.kernel.proof.SCProof
-import lisa.kernel.proof.SCProofCheckerJudgement
-import lisa.kernel.proof.SCProofCheckerJudgement.*
-import lisa.kernel.proof.SequentCalculus.*
-
-/**
- * A set of methods to pretty-print kernel trees.
- */
-object Printer {
-
-  private def spaceSeparator(compact: Boolean): String = if (compact) "" else " "
-  private def commaSeparator(compact: Boolean, symbol: String = ","): String = s"$symbol${spaceSeparator(compact)}"
-
-  private def prettyParentheses(content: String): String = s"(${content})"
-
-  private def prettyFunction(name: String, args: Seq[String], compact: Boolean, dropParentheses: Boolean = true): String = {
-    if (dropParentheses && args.isEmpty) name else s"$name(${args.mkString(commaSeparator(compact))})"
-  }
-
-  private def prettyInfix(operator: String, left: String, right: String, compact: Boolean): String =
-    Seq(left, operator, right).mkString(spaceSeparator(compact))
-
-  // Special symbols that aren't defined in this theory
-  private val (membership, subsetOf, sameCardinality) = (
-    ConstantPredicateLabel("set_membership", 2),
-    ConstantPredicateLabel("subset_of", 2),
-    ConstantPredicateLabel("same_cardinality", 2)
-  )
-  private val (emptySet, unorderedPair, orderedPair, singleton, powerSet, unionSet) = (
-    ConstantFunctionLabel("empty_set", 0),
-    ConstantFunctionLabel("unordered_pair", 2),
-    ConstantFunctionLabel("ordered_pair", 2),
-    ConstantFunctionLabel("singleton", 1),
-    ConstantFunctionLabel("power_set", 1),
-    ConstantFunctionLabel("union", 1)
-  )
-  private val nonAtomicPredicates: Set[PredicateLabel] = Set(equality, membership, subsetOf, sameCardinality) // Predicates which require parentheses (for readability)
-
-  private def prettyFormulaInternal(formula: Formula, isRightMost: Boolean, compact: Boolean): String = formula match {
-    case PredicateFormula(label, args) =>
-      label match {
-        case `equality` =>
-          args match {
-            case Seq(l, r) => prettyInfix(label.id, prettyTerm(l), prettyTerm(r), compact)
-            case _ => throw new Exception
-          }
-        case `membership` =>
-          args match {
-            case Seq(l, r) => prettyInfix("∈", prettyTerm(l), prettyTerm(r), compact)
-            case _ => throw new Exception
-          }
-        case `subsetOf` =>
-          args match {
-            case Seq(l, r) => prettyInfix("⊆", prettyTerm(l), prettyTerm(r), compact)
-            case _ => throw new Exception
-          }
-        case `sameCardinality` =>
-          args match {
-            case Seq(l, r) => prettyInfix("~", prettyTerm(l), prettyTerm(r), compact)
-            case _ => throw new Exception
-          }
-        case _ =>
-          val labelString = label match {
-            case ConstantPredicateLabel(id, _) => id
-            case SchematicPredicateLabel(id, _) => s"?$id"
-          }
-          prettyFunction(labelString, args.map(prettyTerm(_, compact)), compact)
-      }
-    case ConnectorFormula(label, args) =>
-      (label, args) match {
-        case (Neg, Seq(arg)) =>
-          val isAtomic = arg match {
-            case PredicateFormula(label, _) => !nonAtomicPredicates.contains(label)
-            case ConnectorFormula(Neg, _) => true
-            case _ => false
-          }
-          val bodyString = prettyFormulaInternal(arg, isRightMost, compact)
-          val bodyParenthesized = if (isAtomic) bodyString else prettyParentheses(bodyString)
-          s"${label.id}${bodyParenthesized}"
-        case (binary @ (Implies | Iff | And | Or), Seq(l, r)) =>
-          val precedences: Map[ConnectorLabel, Int] = Map(
-            And -> 1,
-            Or -> 2,
-            Implies -> 3,
-            Iff -> 4
-          )
-          val precedence = precedences(binary)
-          val isLeftParentheses = l match {
-            case _: BinderFormula => true
-            case PredicateFormula(leftLabel, _) => nonAtomicPredicates.contains(leftLabel)
-            case ConnectorFormula(leftLabel, _) => precedences.get(leftLabel).exists(_ >= precedence)
-          }
-          val isRightParentheses = r match {
-            case _: BinderFormula => !isRightMost
-            case PredicateFormula(leftLabel, _) => nonAtomicPredicates.contains(leftLabel)
-            case ConnectorFormula(rightLabel, _) => precedences.get(rightLabel).exists(_ > precedence)
-          }
-          val (leftString, rightString) = (prettyFormulaInternal(l, isLeftParentheses, compact), prettyFormulaInternal(r, isRightMost || isRightParentheses, compact))
-          val leftParenthesized = if (isLeftParentheses) prettyParentheses(leftString) else leftString
-          val rightParenthesized = if (isRightParentheses) prettyParentheses(rightString) else rightString
-          prettyInfix(label.id, leftParenthesized, rightParenthesized, compact)
-        case (nary @ (And | Or), args) if args.nonEmpty =>
-          // Rewriting to match the above case; namely op(a) --> a, and op(a, ...rest) --> op(a, op(...rest))
-          // Empty args aren't allowed here
-          // Invariant: args.size > 2
-          if (args.sizeIs == 1) {
-            prettyFormulaInternal(args.head, isRightMost, compact)
-          } else {
-            prettyFormulaInternal(ConnectorFormula(nary, Seq(args.head, ConnectorFormula(nary, args.tail))), isRightMost, compact)
-          }
-        case _ => prettyFunction(label.id, args.map(a => prettyFormulaInternal(a, isRightMost, compact)), compact)
-      }
-    case BinderFormula(label, bound, inner) =>
-      def accumulateNested(f: Formula, acc: Seq[VariableLabel]): (Seq[VariableLabel], Formula) = f match {
-        case BinderFormula(`label`, nestBound, nestInner) => accumulateNested(nestInner, nestBound +: acc)
-        case _ => (acc, f)
-      }
-      val (bounds, innerNested) = accumulateNested(inner, Seq(bound))
-      Seq(s"${label.id}${bounds.reverse.map(_.id).mkString(commaSeparator(compact))}.", prettyFormulaInternal(innerNested, true, compact)).mkString(spaceSeparator(compact))
-  }
-
-  /**
-   * Returns a string representation of this formula. See also [[prettyTerm]].
-   * Example output:
-   * <pre>
-   * ∀x, y. (∀z. (z ∈ x) ↔ (z ∈ y)) ↔ (x = y)
-   * </pre>
-   * @param formula the formula
-   * @param compact whether spaces should be omitted between tokens
-   * @return the string representation of this formula
-   */
-  def prettyFormula(formula: Formula, compact: Boolean = false): String = prettyFormulaInternal(formula, true, compact)
-
-  /**
-   * Returns a string representation of this term. See also [[prettyFormula]].
-   * Example output:
-   * <pre>
-   * f({w, (x, y)}, z)
-   * </pre>
-   * @param term the term
-   * @param compact whether spaces should be omitted between tokens
-   * @return the string representation of this term
-   */
-  def prettyTerm(term: Term, compact: Boolean = false): String = term match {
-    case VariableTerm(label) => label.id
-    case FunctionTerm(label, args) =>
-      label match {
-        case `emptySet` =>
-          args match {
-            case Seq() => prettyFunction("∅", Seq.empty, compact, dropParentheses = true)
-            case _ => throw new Exception
-          }
-        case `unorderedPair` =>
-          args match {
-            case Seq(l, r) => s"{${Seq(l, r).map(prettyTerm(_, compact)).mkString(commaSeparator(compact))}}"
-            case _ => throw new Exception
-          }
-        case `orderedPair` =>
-          args match {
-            case Seq(l, r) => s"(${Seq(l, r).map(prettyTerm(_, compact)).mkString(commaSeparator(compact))})"
-            case _ => throw new Exception
-          }
-        case `singleton` =>
-          args match {
-            case Seq(s) => s"{${prettyTerm(s)}}"
-            case _ => throw new Exception
-          }
-        case `powerSet` =>
-          args match {
-            case Seq(s) => prettyFunction("P", Seq(prettyTerm(s)), compact)
-            case _ => throw new Exception
-          }
-        case `unionSet` =>
-          args match {
-            case Seq(s) => prettyFunction("U", Seq(prettyTerm(s)), compact)
-            case _ => throw new Exception
-          }
-        case _ =>
-          val labelString = label match {
-            case ConstantFunctionLabel(id, _) => id
-            case SchematicFunctionLabel(id, _) => s"?$id"
-          }
-          prettyFunction(labelString, args.map(prettyTerm(_, compact)), compact)
-      }
-  }
-
-  /**
-   * Returns a string representation of this sequent.
-   * Example output:
-   * <pre>
-   * ⊢ ∀x, y. (∀z. (z ∈ x) ↔ (z ∈ y)) ↔ (x = y)
-   * </pre>
-   * @param sequent the sequent
-   * @param compact whether spaces should be omitted between tokens
-   * @return the string representation of this sequent
-   */
-  def prettySequent(sequent: Sequent, compact: Boolean = false): String = {
-    def prettyFormulas(set: Set[Formula]): String = set.toSeq.map(prettyFormula(_, compact)).sorted.mkString(commaSeparator(compact, ";"))
-    Seq(prettyFormulas(sequent.left), "⊢", prettyFormulas(sequent.right)).filter(_.nonEmpty).mkString(spaceSeparator(compact))
-  }
-
-  /**
-   * Returns a string representation of the line number in a proof.
-   * Example output:
-   * <pre>
-   * 0:2:1
-   * </pre>
-   * @param line the line number
-   * @return the string representation of this line number
-   */
-  def prettyLineNumber(line: Seq[Int]): String = line.mkString(":")
-
-  /**
-   * Returns a string representation of this proof.
-   * @param proof the proof
-   * @param judgement optionally provide a proof checking judgement that will mark a particular step in the proof
-   *                  (`->`) as an error. The proof is considered to be valid by default
-   * @return a string where each indented line corresponds to a step in the proof
-   */
-  def prettySCProof(proof: SCProof, judgement: SCProofCheckerJudgement = SCValidProof, forceDisplaySubproofs: Boolean = false): String = {
-    def computeMaxNumberingLengths(proof: SCProof, level: Int, result: IndexedSeq[Int]): IndexedSeq[Int] = {
-      val resultWithCurrent = result.updated(
-        level,
-        (Seq((proof.steps.size - 1).toString.length, result(level)) ++ (if (proof.imports.nonEmpty) Seq((-proof.imports.size).toString.length) else Seq.empty)).max
-      )
-      proof.steps.collect { case sp: SCSubproof => sp }.foldLeft(resultWithCurrent)((acc, sp) => computeMaxNumberingLengths(sp.sp, level + 1, if (acc.size <= level + 1) acc :+ 0 else acc))
-    }
-    val maxNumberingLengths = computeMaxNumberingLengths(proof, 0, IndexedSeq(0)) // The maximum value for each number column
-    val maxLevel = maxNumberingLengths.size - 1
-
-    def leftPadSpaces(v: Any, n: Int): String = {
-      val s = String.valueOf(v)
-      if (s.length < n) (" " * (n - s.length)) + s else s
-    }
-    def rightPadSpaces(v: Any, n: Int): String = {
-      val s = String.valueOf(v)
-      if (s.length < n) s + (" " * (n - s.length)) else s
-    }
-    def prettySCProofRecursive(proof: SCProof, level: Int, tree: IndexedSeq[Int], topMostIndices: IndexedSeq[Int]): Seq[(Boolean, String, String, String)] = {
-      val printedImports = proof.imports.zipWithIndex.reverse.flatMap { case (imp, i) =>
-        val currentTree = tree :+ (-i - 1)
-        val showErrorForLine = judgement match {
-          case SCValidProof => false
-          case SCInvalidProof(position, _) => currentTree.startsWith(position) && currentTree.drop(position.size).forall(_ == 0)
-        }
-        val prefix = (Seq.fill(level - topMostIndices.size)(None) ++ Seq.fill(topMostIndices.size)(None) :+ Some(-i - 1)) ++ Seq.fill(maxLevel - level)(None)
-        val prefixString = prefix.map(_.map(_.toString).getOrElse("")).zipWithIndex.map { case (v, i1) => leftPadSpaces(v, maxNumberingLengths(i1)) }.mkString(" ")
-        def pretty(stepName: String, topSteps: Int*): (Boolean, String, String, String) =
-          (
-            showErrorForLine,
-            prefixString,
-            Seq(stepName, topSteps.mkString(commaSeparator(compact = false))).filter(_.nonEmpty).mkString(" "),
-            prettySequent(imp)
-          )
-
-        Seq(pretty("Import", 0))
-      }
-      printedImports ++ proof.steps.zipWithIndex.flatMap { case (step, i) =>
-        val currentTree = tree :+ i
-        val showErrorForLine = judgement match {
-          case SCValidProof => false
-          case SCInvalidProof(position, _) => currentTree.startsWith(position) && currentTree.drop(position.size).forall(_ == 0)
-        }
-        val prefix = (Seq.fill(level - topMostIndices.size)(None) ++ Seq.fill(topMostIndices.size)(None) :+ Some(i)) ++ Seq.fill(maxLevel - level)(None)
-        val prefixString = prefix.map(_.map(_.toString).getOrElse("")).zipWithIndex.map { case (v, i1) => leftPadSpaces(v, maxNumberingLengths(i1)) }.mkString(" ")
-        def pretty(stepName: String, topSteps: Int*): (Boolean, String, String, String) =
-          (
-            showErrorForLine,
-            prefixString,
-            Seq(stepName, topSteps.mkString(commaSeparator(compact = false))).filter(_.nonEmpty).mkString(" "),
-            prettySequent(step.bot)
-          )
-        step match {
-          case sp @ SCSubproof(_, _, display) if display || forceDisplaySubproofs =>
-            pretty("Subproof", sp.premises*) +: prettySCProofRecursive(sp.sp, level + 1, currentTree, (if (i == 0) topMostIndices else IndexedSeq.empty) :+ i)
-          case other =>
-            val line = other match {
-              case Rewrite(_, t1) => pretty("Rewrite", t1)
-              case Hypothesis(_, _) => pretty("Hypo.")
-              case Cut(_, t1, t2, _) => pretty("Cut", t1, t2)
-              case LeftAnd(_, t1, _, _) => pretty("Left ∧", t1)
-              case LeftNot(_, t1, _) => pretty("Left ¬", t1)
-              case RightOr(_, t1, _, _) => pretty("Right ∨", t1)
-              case RightNot(_, t1, _) => pretty("Right ¬", t1)
-              case LeftExists(_, t1, _, _) => pretty("Left ∃", t1)
-              case LeftForall(_, t1, _, _, _) => pretty("Left ∀", t1)
-              case LeftExistsOne(_, t1, _, _) => pretty("Left ∃!", t1)
-              case LeftOr(_, l, _) => pretty("Left ∨", l*)
-              case RightExists(_, t1, _, _, _) => pretty("Right ∃", t1)
-              case RightForall(_, t1, _, _) => pretty("Right ∀", t1)
-              case RightExistsOne(_, t1, _, _) => pretty("Right ∃!", t1)
-              case RightAnd(_, l, _) => pretty("Right ∧", l*)
-              case RightIff(_, t1, t2, _, _) => pretty("Right ↔", t1, t2)
-              case RightImplies(_, t1, _, _) => pretty("Right →", t1)
-              case Weakening(_, t1) => pretty("Weakening", t1)
-              case LeftImplies(_, t1, t2, _, _) => pretty("Left →", t1, t2)
-              case LeftIff(_, t1, _, _) => pretty("Left ↔", t1)
-              case LeftRefl(_, t1, _) => pretty("L. Refl", t1)
-              case RightRefl(_, _) => pretty("R. Refl")
-              case LeftSubstEq(_, t1, _, _) => pretty("L. SubstEq", t1)
-              case RightSubstEq(_, t1, _, _) => pretty("R. SubstEq", t1)
-              case LeftSubstIff(_, t1, _, _) => pretty("L. SubstIff", t1)
-              case RightSubstIff(_, t1, _, _) => pretty("R. SubstIff", t1)
-              case InstFunSchema(_, t1, _) => pretty("?Fun Instantiation", t1)
-              case InstPredSchema(_, t1, _) => pretty("?Pred Instantiation", t1)
-              case SCSubproof(_, _, false) => pretty("Subproof (hidden)")
-              case other => throw new Exception(s"No available method to print this proof step, consider updating Printer.scala\n$other")
-            }
-            Seq(line)
-        }
-      }
-    }
-
-    val marker = "->"
-
-    val lines = prettySCProofRecursive(proof, 0, IndexedSeq.empty, IndexedSeq.empty)
-    val maxStepNameLength = lines.map { case (_, _, stepName, _) => stepName.length }.maxOption.getOrElse(0)
-    lines
-      .map { case (isMarked, indices, stepName, sequent) =>
-        val suffix = Seq(indices, rightPadSpaces(stepName, maxStepNameLength), sequent)
-        val full = if (!judgement.isValid) (if (isMarked) marker else leftPadSpaces("", marker.length)) +: suffix else suffix
-        full.mkString(" ")
-      }
-      .mkString("\n") + (judgement match {
-      case SCValidProof => ""
-      case SCInvalidProof(path, message) => s"\nProof checker has reported an error at line ${path.mkString(".")}: $message"
-    })
-  }
-
-}
diff --git a/src/main/scala/lisa/kernel/proof/Judgement.scala b/src/main/scala/lisa/kernel/proof/Judgement.scala
index 680d70b4..56137f41 100644
--- a/src/main/scala/lisa/kernel/proof/Judgement.scala
+++ b/src/main/scala/lisa/kernel/proof/Judgement.scala
@@ -8,6 +8,7 @@ import lisa.kernel.proof.RunningTheory
  */
 sealed abstract class SCProofCheckerJudgement {
   import SCProofCheckerJudgement.*
+  val proof: SCProof
 
   /**
    * Whether this judgement is positive -- the proof is concluded to be valid;
@@ -15,7 +16,7 @@ sealed abstract class SCProofCheckerJudgement {
    * @return An instance of either [[SCValidProof]] or [[SCInvalidProof]]
    */
   def isValid: Boolean = this match {
-    case SCValidProof => true
+    case _: SCValidProof => true
     case _: SCInvalidProof => false
   }
 }
@@ -25,14 +26,14 @@ object SCProofCheckerJudgement {
   /**
    * A positive judgement.
    */
-  case object SCValidProof extends SCProofCheckerJudgement
+  case class SCValidProof(proof: SCProof) extends SCProofCheckerJudgement
 
   /**
    * A negative judgement.
    * @param path The path of the error, expressed as indices
    * @param message The error message that hints about the first error encountered
    */
-  case class SCInvalidProof(path: Seq[Int], message: String) extends SCProofCheckerJudgement
+  case class SCInvalidProof(proof: SCProof, path: Seq[Int], message: String) extends SCProofCheckerJudgement
 }
 
 /**
diff --git a/src/main/scala/lisa/kernel/proof/RunningTheory.scala b/src/main/scala/lisa/kernel/proof/RunningTheory.scala
index 70f54f3c..dd307f14 100644
--- a/src/main/scala/lisa/kernel/proof/RunningTheory.scala
+++ b/src/main/scala/lisa/kernel/proof/RunningTheory.scala
@@ -62,21 +62,26 @@ class RunningTheory {
 
   private[proof] val theoryAxioms: mMap[String, Axiom] = mMap.empty
   private[proof] val theorems: mMap[String, Theorem] = mMap.empty
-  private[proof] val definitions: mMap[ConstantLabel, Option[Definition]] = mMap(equality -> None)
+  private[proof] val funDefinitions: mMap[ConstantFunctionLabel, Option[FunctionDefinition]] = mMap.empty
+  private[proof] val predDefinitions: mMap[ConstantPredicateLabel, Option[PredicateDefinition]] = mMap(equality -> None)
 
   /**
    * Check if a label is a symbol of the theory
    */
-  def isSymbol(label: ConstantLabel): Boolean = definitions.contains(label)
 
-  /**
-   * From a given proof, if it is true in the Running theory, add that theorem to the theory and returns it.
-   * The proof's imports must be justified by the list of justification, and the conclusion of the theorem
-   * can't contain symbols that do not belong to the theory.
-   * @param justifications The list of justifications of the proof's imports.
-   * @param proof The proof of the desired Theorem.
-   * @return A Theorem if the proof is correct, None else
-   */
+  def isSymbol(label: ConstantLabel): Boolean = label match
+    case c: ConstantFunctionLabel => funDefinitions.contains(c)
+    case c: ConstantPredicateLabel => predDefinitions.contains(c)
+
+    /**
+     * From a given proof, if it is true in the Running theory, add that theorem to the theory and returns it.
+     * The proof's imports must be justified by the list of justification, and the conclusion of the theorem
+     * can't contain symbols that do not belong to the theory.
+     *
+     * @param justifications The list of justifications of the proof's imports.
+     * @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] = {
     if (proof.conclusion == statement) proofToTheorem(name, proof, justifications)
     else InvalidJustification("The proof does not prove the claimed statement", None)
@@ -87,11 +92,11 @@ class RunningTheory {
       if (belongsToTheory(proof.conclusion))
         val r = SCProofChecker.checkSCProof(proof)
         r match {
-          case SCProofCheckerJudgement.SCValidProof =>
+          case SCProofCheckerJudgement.SCValidProof(_) =>
             val thm = Theorem(name, proof.conclusion)
             theorems.update(name, thm)
             ValidJustification(thm)
-          case r @ SCProofCheckerJudgement.SCInvalidProof(path, 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)
@@ -100,9 +105,10 @@ class RunningTheory {
   /**
    * Introduce a new definition of a predicate in the theory. The symbol must not already exist in the theory
    * and the formula can't contain symbols that are not in the theory.
+   *
    * @param label The desired label.
-   * @param args The variables representing the arguments of the predicate in the formula phi.
-   * @param phi The formula defining the predicate.
+   * @param args  The variables representing the arguments of the predicate in the formula phi.
+   * @param phi   The formula defining the predicate.
    * @return A definition object if the parameters are correct,
    */
   def makePredicateDefinition(label: ConstantPredicateLabel, args: Seq[VariableLabel], phi: Formula): RunningTheoryJudgement[this.PredicateDefinition] = {
@@ -110,7 +116,7 @@ class RunningTheory {
       if (!isSymbol(label))
         if (phi.freeVariables.subsetOf(args.toSet) && phi.schematicFunctions.isEmpty && phi.schematicPredicates.isEmpty)
           val newDef = PredicateDefinition(label, args, phi)
-          definitions.update(label, Some(newDef))
+          predDefinitions.update(label, Some(newDef))
           RunningTheoryJudgement.ValidJustification(newDef)
         else InvalidJustification("The definition is not allowed to contain schematic symbols or free variables.", None)
       else InvalidJustification("The specified symbol is already part of the theory and can't be redefined.", None)
@@ -123,12 +129,13 @@ class RunningTheory {
    * satisfying the definition's formula must first be proven. This is easy if the formula behaves as a shortcut,
    * for example f(x,y) = 3x+2y
    * but is much more general. The proof's conclusion must be of the form:  |- ∀args. ∃!out. phi
-   * @param proof The proof of existence and uniqueness
+   *
+   * @param proof          The proof of existence and uniqueness
    * @param justifications The justifications of the proof.
-   * @param label The desired label.
-   * @param args The variables representing the arguments of the predicate in the formula phi.
-   * @param out The variable representing the function's result in the formula
-   * @param phi The formula defining the predicate.
+   * @param label          The desired label.
+   * @param args           The variables representing the arguments of the predicate in the formula phi.
+   * @param out            The variable representing the function's result in the formula
+   * @param phi            The formula defining the predicate.
    * @return A definition object if the parameters are correct,
    */
   def makeFunctionDefinition(
@@ -145,19 +152,19 @@ class RunningTheory {
           if (proof.imports.forall(i => justifications.exists(j => isSameSequent(i, sequentFromJustification(j)))))
             val r = SCProofChecker.checkSCProof(proof)
             r match {
-              case SCProofCheckerJudgement.SCValidProof =>
+              case SCProofCheckerJudgement.SCValidProof(_) =>
                 proof.conclusion match {
                   case Sequent(l, r) if l.isEmpty && r.size == 1 =>
                     val subst = bindAll(Forall, args, BinderFormula(ExistsOne, out, phi))
                     val subst2 = bindAll(Forall, args.reverse, BinderFormula(ExistsOne, out, phi))
                     if (isSame(r.head, subst) || isSame(r.head, subst2)) {
                       val newDef = FunctionDefinition(label, args, out, phi)
-                      definitions.update(label, Some(newDef))
+                      funDefinitions.update(label, Some(newDef))
                       RunningTheoryJudgement.ValidJustification(newDef)
                     } 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)
@@ -194,6 +201,7 @@ class RunningTheory {
 
   /**
    * Verify if a given formula belongs to some language
+   *
    * @param phi The formula to check
    * @return Weather phi belongs to the specified language
    */
@@ -214,6 +222,7 @@ class RunningTheory {
 
   /**
    * Verify if a given term belongs to some language
+   *
    * @param t The term to check
    * @return Weather t belongs to the specified language
    */
@@ -229,6 +238,7 @@ class RunningTheory {
 
   /**
    * Verify if a given sequent belongs to some language
+   *
    * @param s The sequent to check
    * @return Weather s belongs to the specified language
    */
@@ -244,6 +254,7 @@ class RunningTheory {
    * Add a new axiom to the Theory. For example, if the theory contains the language and theorems
    * of Zermelo-Fraenkel Set Theory, this function can add the axiom of choice to it.
    * If the axiom belongs to the language of the theory, adds it and return true. Else, returns false.
+   *
    * @param f the new axiom to be added.
    * @return true if the axiom was added to the theory, false else.
    */
@@ -260,28 +271,38 @@ class RunningTheory {
    * For example, This function can add the empty set symbol to a theory, and then an axiom asserting
    * the it is empty can be introduced as well.
    */
-  def addSymbol(s: ConstantLabel): Unit = definitions.update(s, None)
+
+  def addSymbol(s: ConstantLabel): Unit = s match
+    case c: ConstantFunctionLabel => funDefinitions.update(c, None)
+    case c: ConstantPredicateLabel => predDefinitions.update(c, None)
 
   /**
    * Public accessor to the set of symbol currently in the theory's language.
+   *
    * @return the set of symbol currently in the theory's language.
    */
-  def language: List[(ConstantLabel, Option[Definition])] = definitions.toList
+
+  def language: List[(ConstantLabel, Option[Definition])] = funDefinitions.toList ++ predDefinitions.toList
 
   /**
    * Public accessor to the current set of axioms of the theory
+   *
    * @return the current set of axioms of the theory
    */
   def axiomsList: Iterable[Axiom] = theoryAxioms.values
 
   /**
    * Verify if a given formula is an axiom of the theory
+   *
    * @param f the candidate axiom
    * @return wether f is an axiom of the theory
    */
   def isAxiom(f: Formula): Boolean = theoryAxioms.exists(a => isSame(a._2.ax, f))
+
   def getAxiom(f: Formula): Option[Axiom] = theoryAxioms.find(a => isSame(a._2.ax, f)).map(_._2)
+
   def getAxiom(name: String): Option[Axiom] = theoryAxioms.get(name)
+
   def getTheorem(name: String): Option[Theorem] = theorems.get(name)
 
 }
diff --git a/src/main/scala/lisa/kernel/proof/SCProofChecker.scala b/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
index ad72abfe..1ae79196 100644
--- a/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
+++ b/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
@@ -1,9 +1,9 @@
 package lisa.kernel.proof
 
-import lisa.kernel.Printer
 import lisa.kernel.fol.FOL.*
 import lisa.kernel.proof.SCProofCheckerJudgement.*
 import lisa.kernel.proof.SequentCalculus.*
+import utilities.Printer
 
 object SCProofChecker {
 
@@ -28,9 +28,9 @@ object SCProofChecker {
 
     val r: SCProofCheckerJudgement =
       if (false_premise.nonEmpty)
-        SCInvalidProof(Nil, s"Step no $no can't refer to higher number ${false_premise.get} as a premise.")
+        SCInvalidProof(SCProof(step), Nil, s"Step no $no can't refer to higher number ${false_premise.get} as a premise.")
       else if (false_premise2.nonEmpty)
-        SCInvalidProof(Nil, s"A step can't refer to step ${false_premise2.get}, imports only contains ${importsSize.get} elements.")
+        SCInvalidProof(SCProof(step), Nil, s"A step can't refer to step ${false_premise2.get}, imports only contains ${importsSize.get} elements.")
       else
         step match {
           /*
@@ -39,7 +39,7 @@ object SCProofChecker {
            *    Γ |- Δ
            */
           case Rewrite(s, t1) =>
-            if (isSameSequent(s, ref(t1))) SCValidProof else SCInvalidProof(Nil, s"The premise and the conclusion are not trivially equivalent.")
+            if (isSameSequent(s, ref(t1))) SCValidProof(SCProof(step)) else SCInvalidProof(SCProof(step), Nil, s"The premise and the conclusion are not trivially equivalent.")
           /*
            *
            * --------------
@@ -47,9 +47,9 @@ object SCProofChecker {
            */
           case Hypothesis(Sequent(left, right), phi) =>
             if (contains(left, phi))
-              if (contains(right, phi)) SCValidProof
-              else SCInvalidProof(Nil, s"Right-hand side does not contain formula φ")
-            else SCInvalidProof(Nil, s"Left-hand side does not contain formula φ")
+              if (contains(right, phi)) SCValidProof(SCProof(step))
+              else SCInvalidProof(SCProof(step), Nil, s"Right-hand side does not contain formula φ")
+            else SCInvalidProof(SCProof(step), Nil, s"Left-hand side does not contain formula φ")
           /*
            *  Γ |- Δ, φ    φ, Σ |- Π
            * ------------------------
@@ -60,11 +60,11 @@ object SCProofChecker {
               if (isSameSet(b.right, ref(t2).right union ref(t1).right.filterNot(isSame(_, phi))))
                 if (contains(ref(t2).left, phi))
                   if (contains(ref(t1).right, phi))
-                    SCValidProof
-                  else SCInvalidProof(Nil, s"Right-hand side of first premise does not contain φ as claimed.")
-                else SCInvalidProof(Nil, s"Left-hand side of second premise does not contain φ as claimed.")
-              else SCInvalidProof(Nil, s"Right-hand side of conclusion + φ is not the union of the right-hand sides of the premises.")
-            else SCInvalidProof(Nil, s"Left-hand side of conclusion + φ is not the union of the left-hand sides of the premises.")
+                    SCValidProof(SCProof(step))
+                  else SCInvalidProof(SCProof(step), Nil, s"Right-hand side of first premise does not contain φ as claimed.")
+                else SCInvalidProof(SCProof(step), Nil, s"Left-hand side of second premise does not contain φ as claimed.")
+              else SCInvalidProof(SCProof(step), Nil, s"Right-hand side of conclusion + φ is not the union of the right-hand sides of the premises.")
+            else SCInvalidProof(SCProof(step), Nil, s"Left-hand side of conclusion + φ is not the union of the left-hand sides of the premises.")
 
           // Left rules
           /*
@@ -80,9 +80,9 @@ object SCProofChecker {
                 isSameSet(b.left + psi, ref(t1).left + phiAndPsi) ||
                 isSameSet(b.left + phi + psi, ref(t1).left + phiAndPsi)
               )
-                SCValidProof
-              else SCInvalidProof(Nil, "Left-hand side of conclusion + φ∧ψ must be same as left-hand side of premise + either φ, ψ or both.")
-            else SCInvalidProof(Nil, "Right-hand sides of the premise and the conclusion must be the same.")
+                SCValidProof(SCProof(step))
+              else SCInvalidProof(SCProof(step), Nil, "Left-hand side of conclusion + φ∧ψ must be same as left-hand side of premise + either φ, ψ or both.")
+            else SCInvalidProof(SCProof(step), Nil, "Right-hand sides of the premise and the conclusion must be the same.")
           /*
            *  Γ, φ |- Δ    Σ, ψ |- Π
            * ------------------------
@@ -92,9 +92,9 @@ object SCProofChecker {
             if (isSameSet(b.right, t.map(ref(_).right).reduce(_ union _)))
               val phiOrPsi = ConnectorFormula(Or, disjuncts)
               if (isSameSet(disjuncts.foldLeft(b.left)(_ + _), t.map(ref(_).left).reduce(_ union _) + phiOrPsi))
-                SCValidProof
-              else SCInvalidProof(Nil, s"Left-hand side of conclusion + disjuncts is not the same as the union of the left-hand sides of the premises + φ∨ψ.")
-            else SCInvalidProof(Nil, s"Right-hand side of conclusion is not the union of the right-hand sides of the premises.")
+                SCValidProof(SCProof(step))
+              else SCInvalidProof(SCProof(step), Nil, s"Left-hand side of conclusion + disjuncts is not the same as the union of the left-hand sides of the premises + φ∨ψ.")
+            else SCInvalidProof(SCProof(step), Nil, s"Right-hand side of conclusion is not the union of the right-hand sides of the premises.")
           /*
            *  Γ |- φ, Δ    Σ, ψ |- Π
            * ------------------------
@@ -104,9 +104,9 @@ object SCProofChecker {
             val phiImpPsi = ConnectorFormula(Implies, Seq(phi, psi))
             if (isSameSet(b.right + phi, ref(t1).right union ref(t2).right))
               if (isSameSet(b.left + psi, ref(t1).left union ref(t2).left + phiImpPsi))
-                SCValidProof
-              else SCInvalidProof(Nil, s"Left-hand side of conclusion + ψ must be identical to union of left-hand sides of premisces + φ→ψ.")
-            else SCInvalidProof(Nil, s"Right-hand side of conclusion + φ must be identical to union of right-hand sides of premisces.")
+                SCValidProof(SCProof(step))
+              else SCInvalidProof(SCProof(step), Nil, s"Left-hand side of conclusion + ψ must be identical to union of left-hand sides of premisces + φ→ψ.")
+            else SCInvalidProof(SCProof(step), Nil, s"Right-hand side of conclusion + φ must be identical to union of right-hand sides of premisces.")
           /*
            *  Γ, φ→ψ |- Δ               Γ, φ→ψ, ψ→φ |- Δ
            * --------------    or     ---------------
@@ -122,9 +122,9 @@ object SCProofChecker {
                 isSameSet(b.left + psiImpPhi, ref(t1).left + phiIffPsi) ||
                 isSameSet(b.left + phiImpPsi + psiImpPhi, ref(t1).left + phiIffPsi)
               )
-                SCValidProof
-              else SCInvalidProof(Nil, "Left-hand side of conclusion + φ↔ψ must be same as left-hand side of premise + either φ→ψ, ψ→φ or both.")
-            else SCInvalidProof(Nil, "Right-hand sides of premise and conclusion must be the same.")
+                SCValidProof(SCProof(step))
+              else SCInvalidProof(SCProof(step), Nil, "Left-hand side of conclusion + φ↔ψ must be same as left-hand side of premise + either φ→ψ, ψ→φ or both.")
+            else SCInvalidProof(SCProof(step), Nil, "Right-hand sides of premise and conclusion must be the same.")
 
           /*
            *   Γ |- φ, Δ
@@ -135,9 +135,9 @@ object SCProofChecker {
             val nPhi = ConnectorFormula(Neg, Seq(phi))
             if (isSameSet(b.left, ref(t1).left + nPhi))
               if (isSameSet(b.right + phi, ref(t1).right))
-                SCValidProof
-              else SCInvalidProof(Nil, "Right-hand side of conclusion + φ must be the same as right-hand side of premise")
-            else SCInvalidProof(Nil, "Left-hand side of conclusion must be the same as left-hand side of premise + ¬φ")
+                SCValidProof(SCProof(step))
+              else SCInvalidProof(SCProof(step), Nil, "Right-hand side of conclusion + φ must be the same as right-hand side of premise")
+            else SCInvalidProof(SCProof(step), Nil, "Left-hand side of conclusion must be the same as left-hand side of premise + ¬φ")
 
           /*
            *   Γ, φ[t/x] |- Δ
@@ -147,9 +147,9 @@ object SCProofChecker {
           case LeftForall(b, t1, phi, x, t) =>
             if (isSameSet(b.right, ref(t1).right))
               if (isSameSet(b.left + substituteVariables(phi, Map(x -> t)), ref(t1).left + BinderFormula(Forall, x, phi)))
-                SCValidProof
-              else SCInvalidProof(Nil, "Left-hand side of conclusion + φ[t/x] must be the same as left-hand side of premise + ∀x. φ")
-            else SCInvalidProof(Nil, "Right-hand side of conclusion must be the same as right-hand side of premise")
+                SCValidProof(SCProof(step))
+              else SCInvalidProof(SCProof(step), Nil, "Left-hand side of conclusion + φ[t/x] must be the same as left-hand side of premise + ∀x. φ")
+            else SCInvalidProof(SCProof(step), Nil, "Right-hand side of conclusion must be the same as right-hand side of premise")
 
           /*
            *    Γ, φ |- Δ
@@ -160,10 +160,10 @@ object SCProofChecker {
             if (isSameSet(b.right, ref(t1).right))
               if (isSameSet(b.left + phi, ref(t1).left + BinderFormula(Exists, x, phi)))
                 if ((b.left union b.right).forall(f => !f.freeVariables.contains(x)))
-                  SCValidProof
-                else SCInvalidProof(Nil, "The variable x must not be free in the resulting sequent.")
-              else SCInvalidProof(Nil, "Left-hand side of conclusion + φ must be the same as left-hand side of premise + ∃x. φ")
-            else SCInvalidProof(Nil, "Right-hand side of conclusion must be the same as right-hand side of premise")
+                  SCValidProof(SCProof(step))
+                else SCInvalidProof(SCProof(step), Nil, "The variable x must not be free in the resulting sequent.")
+              else SCInvalidProof(SCProof(step), Nil, "Left-hand side of conclusion + φ must be the same as left-hand side of premise + ∃x. φ")
+            else SCInvalidProof(SCProof(step), Nil, "Right-hand side of conclusion must be the same as right-hand side of premise")
 
           /*
            *  Γ, ∃y.∀x. (x=y) ↔ φ |-  Δ
@@ -175,9 +175,9 @@ object SCProofChecker {
             val temp = BinderFormula(Exists, y, BinderFormula(Forall, x, ConnectorFormula(Iff, List(PredicateFormula(equality, List(VariableTerm(x), VariableTerm(y))), phi))))
             if (isSameSet(b.right, ref(t1).right))
               if (isSameSet(b.left + temp, ref(t1).left + BinderFormula(ExistsOne, x, phi)))
-                SCValidProof
-              else SCInvalidProof(Nil, "Left-hand side of conclusion + ∃y.∀x. (x=y) ↔ φ must be the same as left-hand side of premise + ∃!x. φ")
-            else SCInvalidProof(Nil, "Right-hand side of conclusion must be the same as right-hand side of premise")
+                SCValidProof(SCProof(step))
+              else SCInvalidProof(SCProof(step), Nil, "Left-hand side of conclusion + ∃y.∀x. (x=y) ↔ φ must be the same as left-hand side of premise + ∃!x. φ")
+            else SCInvalidProof(SCProof(step), Nil, "Right-hand side of conclusion must be the same as right-hand side of premise")
 
           // Right rules
           /*
@@ -189,9 +189,9 @@ object SCProofChecker {
             val phiAndPsi = ConnectorFormula(And, cunjuncts)
             if (isSameSet(b.left, t.map(ref(_).left).reduce(_ union _)))
               if (isSameSet(cunjuncts.foldLeft(b.right)(_ + _), t.map(ref(_).right).reduce(_ union _) + phiAndPsi))
-                SCValidProof
-              else SCInvalidProof(Nil, s"Right-hand side of conclusion + φ + ψ is not the same as the union of the right-hand sides of the premises φ∧ψ.")
-            else SCInvalidProof(Nil, s"Left-hand side of conclusion is not the union of the left-hand sides of the premises.")
+                SCValidProof(SCProof(step))
+              else SCInvalidProof(SCProof(step), Nil, s"Right-hand side of conclusion + φ + ψ is not the same as the union of the right-hand sides of the premises φ∧ψ.")
+            else SCInvalidProof(SCProof(step), Nil, s"Left-hand side of conclusion is not the union of the left-hand sides of the premises.")
           /*
            *   Γ |- φ, Δ                Γ |- φ, ψ, Δ
            * --------------    or    ---------------
@@ -205,9 +205,9 @@ object SCProofChecker {
                 isSameSet(b.right + psi, ref(t1).right + phiOrPsi) ||
                 isSameSet(b.right + phi + psi, ref(t1).right + phiOrPsi)
               )
-                SCValidProof
-              else SCInvalidProof(Nil, "Right-hand side of conclusion + φ∧ψ must be same as right-hand side of premise + either φ, ψ or both.")
-            else SCInvalidProof(Nil, "Left-hand sides of the premise and the conclusion must be the same.")
+                SCValidProof(SCProof(step))
+              else SCInvalidProof(SCProof(step), Nil, "Right-hand side of conclusion + φ∧ψ must be same as right-hand side of premise + either φ, ψ or both.")
+            else SCInvalidProof(SCProof(step), Nil, "Left-hand sides of the premise and the conclusion must be the same.")
           /*
            *  Γ, φ |- ψ, Δ
            * --------------
@@ -217,9 +217,9 @@ object SCProofChecker {
             val phiImpPsi = ConnectorFormula(Implies, Seq(phi, psi))
             if (isSameSet(ref(t1).left, b.left + phi))
               if (isSameSet(b.right + psi, ref(t1).right + phiImpPsi))
-                SCValidProof
-              else SCInvalidProof(Nil, "Right-hand side of conclusion + ψ must be same as right-hand side of premise + φ→ψ.")
-            else SCInvalidProof(Nil, "Left-hand side of conclusion + psi must be same as left-hand side of premise.")
+                SCValidProof(SCProof(step))
+              else SCInvalidProof(SCProof(step), Nil, "Right-hand side of conclusion + ψ must be same as right-hand side of premise + φ→ψ.")
+            else SCInvalidProof(SCProof(step), Nil, "Left-hand side of conclusion + psi must be same as left-hand side of premise.")
           /*
            *  Γ |- a→ψ, Δ    Σ |- ψ→φ, Π
            * ----------------------------
@@ -231,9 +231,9 @@ object SCProofChecker {
             val phiIffPsi = ConnectorFormula(Iff, Seq(phi, psi))
             if (isSameSet(b.left, ref(t1).left union ref(t2).left))
               if (isSameSet(b.right + phiImpPsi + psiImpPhi, ref(t1).right union ref(t2).right + phiIffPsi))
-                SCValidProof
-              else SCInvalidProof(Nil, s"Right-hand side of conclusion + a→ψ + ψ→φ is not the same as the union of the right-hand sides of the premises φ↔b.")
-            else SCInvalidProof(Nil, s"Left-hand side of conclusion is not the union of the left-hand sides of the premises.")
+                SCValidProof(SCProof(step))
+              else SCInvalidProof(SCProof(step), Nil, s"Right-hand side of conclusion + a→ψ + ψ→φ is not the same as the union of the right-hand sides of the premises φ↔b.")
+            else SCInvalidProof(SCProof(step), Nil, s"Left-hand side of conclusion is not the union of the left-hand sides of the premises.")
           /*
            *  Γ, φ |- Δ
            * --------------
@@ -243,9 +243,9 @@ object SCProofChecker {
             val nPhi = ConnectorFormula(Neg, Seq(phi))
             if (isSameSet(b.right, ref(t1).right + nPhi))
               if (isSameSet(b.left + phi, ref(t1).left))
-                SCValidProof
-              else SCInvalidProof(Nil, "Left-hand side of conclusion + φ must be the same as left-hand side of premise")
-            else SCInvalidProof(Nil, "Right-hand side of conclusion must be the same as right-hand side of premise + ¬φ")
+                SCValidProof(SCProof(step))
+              else SCInvalidProof(SCProof(step), Nil, "Left-hand side of conclusion + φ must be the same as left-hand side of premise")
+            else SCInvalidProof(SCProof(step), Nil, "Right-hand side of conclusion must be the same as right-hand side of premise + ¬φ")
           /*
            *    Γ |- φ, Δ
            * ------------------- if x is not free in the resulting sequent
@@ -255,10 +255,10 @@ object SCProofChecker {
             if (isSameSet(b.left, ref(t1).left))
               if (isSameSet(b.right + phi, ref(t1).right + BinderFormula(Forall, x, phi)))
                 if ((b.left union b.right).forall(f => !f.freeVariables.contains(x)))
-                  SCValidProof
-                else SCInvalidProof(Nil, "The variable x must not be free in the resulting sequent.")
-              else SCInvalidProof(Nil, "Right-hand side of conclusion + φ must be the same as right-hand side of premise + ∀x. φ")
-            else SCInvalidProof(Nil, "Left-hand sides of conclusion and premise must be the same.")
+                  SCValidProof(SCProof(step))
+                else SCInvalidProof(SCProof(step), Nil, "The variable x must not be free in the resulting sequent.")
+              else SCInvalidProof(SCProof(step), Nil, "Right-hand side of conclusion + φ must be the same as right-hand side of premise + ∀x. φ")
+            else SCInvalidProof(SCProof(step), Nil, "Left-hand sides of conclusion and premise must be the same.")
           /*
            *   Γ |- φ[t/x], Δ
            * -------------------
@@ -267,9 +267,9 @@ object SCProofChecker {
           case RightExists(b, t1, phi, x, t) =>
             if (isSameSet(b.left, ref(t1).left))
               if (isSameSet(b.right + substituteVariables(phi, Map(x -> t)), ref(t1).right + BinderFormula(Exists, x, phi)))
-                SCValidProof
-              else SCInvalidProof(Nil, "Right-hand side of the conclusion + φ[t/x] must be the same as right-hand side of the premise + ∃x. φ")
-            else SCInvalidProof(Nil, "Left-hand sides or conclusion and premise must be the same.")
+                SCValidProof(SCProof(step))
+              else SCInvalidProof(SCProof(step), Nil, "Right-hand side of the conclusion + φ[t/x] must be the same as right-hand side of the premise + ∃x. φ")
+            else SCInvalidProof(SCProof(step), Nil, "Left-hand sides or conclusion and premise must be the same.")
 
           /**
            * <pre>
@@ -283,9 +283,9 @@ object SCProofChecker {
             val temp = BinderFormula(Exists, y, BinderFormula(Forall, x, ConnectorFormula(Iff, List(PredicateFormula(equality, List(VariableTerm(x), VariableTerm(y))), phi))))
             if (isSameSet(b.left, ref(t1).left))
               if (isSameSet(b.right + temp, ref(t1).right + BinderFormula(ExistsOne, x, phi)))
-                SCValidProof
-              else SCInvalidProof(Nil, "Right-hand side of conclusion + ∃y.∀x. (x=y) ↔ φ must be the same as right-hand side of premise + ∃!x. φ")
-            else SCInvalidProof(Nil, "Left-hand sides of conclusion and premise must be the same")
+                SCValidProof(SCProof(step))
+              else SCInvalidProof(SCProof(step), Nil, "Right-hand side of conclusion + ∃y.∀x. (x=y) ↔ φ must be the same as right-hand side of premise + ∃!x. φ")
+            else SCInvalidProof(SCProof(step), Nil, "Left-hand sides of conclusion and premise must be the same")
 
           // Structural rules
           /*
@@ -296,9 +296,9 @@ object SCProofChecker {
           case Weakening(b, t1) =>
             if (isSubset(ref(t1).left, b.left))
               if (isSubset(ref(t1).right, b.right))
-                SCValidProof
-              else SCInvalidProof(Nil, "Right-hand side of premise must be a subset of right-hand side of conclusion")
-            else SCInvalidProof(Nil, "Left-hand side of premise must be a subset of left-hand side of conclusion")
+                SCValidProof(SCProof(step))
+              else SCInvalidProof(SCProof(step), Nil, "Right-hand side of premise must be a subset of right-hand side of conclusion")
+            else SCInvalidProof(SCProof(step), Nil, "Left-hand side of premise must be a subset of left-hand side of conclusion")
 
           // Equality Rules
           /*
@@ -312,11 +312,11 @@ object SCProofChecker {
                 if (isSame(left, right))
                   if (isSameSet(b.right, ref(t1).right))
                     if (isSameSet(b.left + phi, ref(t1).left))
-                      SCValidProof
-                    else SCInvalidProof(Nil, s"Left-hand sides of the conclusion + φ must be the same as left-hand side of the premise.")
-                  else SCInvalidProof(Nil, s"Right-hand sides of the premise and the conclusion aren't the same.")
-                else SCInvalidProof(Nil, s"φ is not an instance of reflexivity.")
-              case _ => SCInvalidProof(Nil, "φ is not an equality")
+                      SCValidProof(SCProof(step))
+                    else SCInvalidProof(SCProof(step), Nil, s"Left-hand sides of the conclusion + φ must be the same as left-hand side of the premise.")
+                  else SCInvalidProof(SCProof(step), Nil, s"Right-hand sides of the premise and the conclusion aren't the same.")
+                else SCInvalidProof(SCProof(step), Nil, s"φ is not an instance of reflexivity.")
+              case _ => SCInvalidProof(SCProof(step), Nil, "φ is not an equality")
             }
 
           /*
@@ -329,10 +329,10 @@ object SCProofChecker {
               case PredicateFormula(`equality`, Seq(left, right)) =>
                 if (isSame(left, right))
                   if (contains(b.right, phi))
-                    SCValidProof
-                  else SCInvalidProof(Nil, s"Right-Hand side of conclusion does not contain φ")
-                else SCInvalidProof(Nil, s"φ is not an instance of reflexivity.")
-              case _ => SCInvalidProof(Nil, s"φ is not an equality.")
+                    SCValidProof(SCProof(step))
+                  else SCInvalidProof(SCProof(step), Nil, s"Right-Hand side of conclusion does not contain φ")
+                else SCInvalidProof(SCProof(step), Nil, s"φ is not an instance of reflexivity.")
+              case _ => SCInvalidProof(SCProof(step), Nil, s"φ is not an equality.")
             }
 
           /*
@@ -351,9 +351,14 @@ object SCProofChecker {
                 isSameSet(b.left + phi_t_for_f, ref(t1).left ++ sEqT_es + phi_s_for_f) ||
                 isSameSet(b.left + phi_s_for_f, ref(t1).left ++ sEqT_es + phi_t_for_f)
               )
-                SCValidProof
-              else SCInvalidProof(Nil, "Left-hand sides of the conclusion + φ(s_) must be the same as left-hand side of the premise + (s=t)_ + φ(t_) (or with s_ and t_ swapped).")
-            else SCInvalidProof(Nil, "Right-hand sides of the premise and the conclusion aren't the same.")
+                SCValidProof(SCProof(step))
+              else
+                SCInvalidProof(
+                  SCProof(step),
+                  Nil,
+                  "Left-hand sides of the conclusion + φ(s_) must be the same as left-hand side of the premise + (s=t)_ + φ(t_) (or with s_ and t_ swapped)."
+                )
+            else SCInvalidProof(SCProof(step), Nil, "Right-hand sides of the premise and the conclusion aren't the same.")
 
           /*
            *    Γ |- φ(s_), Δ
@@ -370,9 +375,14 @@ object SCProofChecker {
                 isSameSet(b.right + phi_s_for_f, ref(t1).right + phi_t_for_f) ||
                 isSameSet(b.right + phi_t_for_f, ref(t1).right + phi_s_for_f)
               )
-                SCValidProof
-              else SCInvalidProof(Nil, s"Right-hand side of the premise and the conclusion should be the same with each containing one of φ(s_) φ(t_), but it isn't the case.")
-            else SCInvalidProof(Nil, "Left-hand sides of the premise + (s=t)_ must be the same as left-hand side of the premise.")
+                SCValidProof(SCProof(step))
+              else
+                SCInvalidProof(
+                  SCProof(step),
+                  Nil,
+                  s"Right-hand side of the premise and the conclusion should be the same with each containing one of φ(s_) φ(t_), but it isn't the case."
+                )
+            else SCInvalidProof(SCProof(step), Nil, "Left-hand sides of the premise + (s=t)_ must be the same as left-hand side of the premise.")
           /*
            *    Γ, φ(ψ_) |- Δ
            * ---------------------
@@ -388,9 +398,14 @@ object SCProofChecker {
                 isSameSet(ref(t1).left ++ psiIffTau + phi_tau_for_q, b.left + phi_psi_for_q) ||
                 isSameSet(ref(t1).left ++ psiIffTau + phi_psi_for_q, b.left + phi_tau_for_q)
               )
-                SCValidProof
-              else SCInvalidProof(Nil, "Left-hand sides of the conclusion + φ(ψ_) must be the same as left-hand side of the premise + (ψ↔τ)_ + φ(τ_) (or with ψ and τ swapped).")
-            else SCInvalidProof(Nil, "Right-hand sides of the premise and the conclusion aren't the same.")
+                SCValidProof(SCProof(step))
+              else
+                SCInvalidProof(
+                  SCProof(step),
+                  Nil,
+                  "Left-hand sides of the conclusion + φ(ψ_) must be the same as left-hand side of the premise + (ψ↔τ)_ + φ(τ_) (or with ψ and τ swapped)."
+                )
+            else SCInvalidProof(SCProof(step), Nil, "Right-hand sides of the premise and the conclusion aren't the same.")
 
           /*
            *    Γ |- φ[ψ/?p], Δ
@@ -407,9 +422,14 @@ object SCProofChecker {
                 isSameSet(b.right + phi_tau_for_q, ref(t1).right + phi_psi_for_q) ||
                 isSameSet(b.right + phi_psi_for_q, ref(t1).right + phi_tau_for_q)
               )
-                SCValidProof
-              else SCInvalidProof(Nil, s"Right-hand side of the premise and the conclusion should be the same with each containing one of φ[τ/?q] and φ[ψ/?q], but it isn't the case.")
-            else SCInvalidProof(Nil, "Left-hand sides of the premise + ψ↔τ must be the same as left-hand side of the premise.")
+                SCValidProof(SCProof(step))
+              else
+                SCInvalidProof(
+                  SCProof(step),
+                  Nil,
+                  s"Right-hand side of the premise and the conclusion should be the same with each containing one of φ[τ/?q] and φ[ψ/?q], but it isn't the case."
+                )
+            else SCInvalidProof(SCProof(step), Nil, "Left-hand sides of the premise + ψ↔τ must be the same as left-hand side of the premise.")
 
           /**
            * <pre>
@@ -422,9 +442,9 @@ object SCProofChecker {
             val expected = (ref(t1).left.map(phi => instantiateFunctionSchemas(phi, insts)), ref(t1).right.map(phi => instantiateFunctionSchemas(phi, insts)))
             if (isSameSet(bot.left, expected._1))
               if (isSameSet(bot.right, expected._2))
-                SCValidProof
-              else SCInvalidProof(Nil, "Right-hand side of premise instantiated with the map 'insts' must be the same as right-hand side of conclusion.")
-            else SCInvalidProof(Nil, "Left-hand side of premise instantiated with the map 'insts' must be the same as left-hand side of conclusion.")
+                SCValidProof(SCProof(step))
+              else SCInvalidProof(SCProof(step), Nil, "Right-hand side of premise instantiated with the map 'insts' must be the same as right-hand side of conclusion.")
+            else SCInvalidProof(SCProof(step), Nil, "Left-hand side of premise instantiated with the map 'insts' must be the same as left-hand side of conclusion.")
 
           /**
            * <pre>
@@ -437,18 +457,23 @@ object SCProofChecker {
             val expected = (ref(t1).left.map(phi => instantiatePredicateSchemas(phi, insts)), ref(t1).right.map(phi => instantiatePredicateSchemas(phi, insts)))
             if (isSameSet(bot.left, expected._1))
               if (isSameSet(bot.right, expected._2))
-                SCValidProof
+                SCValidProof(SCProof(step))
               else
-                SCInvalidProof(Nil, "Right-hand side of premise instantiated with the map 'insts' must be the same as right-hand side of conclusion.")
-            else SCInvalidProof(Nil, "Left-hand side of premise instantiated with the map 'insts' must be the same as left-hand side of conclusion.")
+                SCInvalidProof(SCProof(step), Nil, "Right-hand side of premise instantiated with the map 'insts' must be the same as right-hand side of conclusion.")
+            else SCInvalidProof(SCProof(step), Nil, "Left-hand side of premise instantiated with the map 'insts' must be the same as left-hand side of conclusion.")
 
           case SCSubproof(sp, premises, _) =>
             if (premises.size == sp.imports.size) {
               val invalid = premises.zipWithIndex.find((no, p) => !isSameSequent(ref(no), sp.imports(p)))
               if (invalid.isEmpty) {
                 checkSCProof(sp)
-              } else SCInvalidProof(Nil, s"Premise number ${invalid.get._1} (refering to step ${invalid.get}) is not the same as import number ${invalid.get._1} of the subproof.")
-            } else SCInvalidProof(Nil, "Number of premises and imports don't match: " + premises.size + " " + sp.imports.size)
+              } else
+                SCInvalidProof(
+                  SCProof(step),
+                  Nil,
+                  s"Premise number ${invalid.get._1} (refering to step ${invalid.get}) is not the same as import number ${invalid.get._1} of the subproof."
+                )
+            } else SCInvalidProof(SCProof(step), Nil, "Number of premises and imports don't match: " + premises.size + " " + sp.imports.size)
 
         }
     r
@@ -459,19 +484,19 @@ object SCProofChecker {
    * If the proof is not correct, the functrion will report the faulty line and a brief explanation.
    *
    * @param proof A SC proof to check
-   * @return SCValidProof if the proof is correct, else SCInvalidProof with the path to the incorrect proof step
+   * @return SCValidProof(SCProof(step)) if the proof is correct, else SCInvalidProof with the path to the incorrect proof step
    *         and an explanation.
    */
   def checkSCProof(proof: SCProof): SCProofCheckerJudgement = {
     val possibleError = proof.steps.view.zipWithIndex
       .map((step, no) =>
         checkSingleSCStep(no, step, (i: Int) => proof.getSequent(i), Some(proof.imports.size)) match {
-          case SCInvalidProof(path, message) => SCInvalidProof(no +: path, message)
-          case SCValidProof => SCValidProof
+          case SCInvalidProof(_, path, message) => SCInvalidProof(proof, no +: path, message)
+          case SCValidProof(_) => SCValidProof(proof)
         }
       )
       .find(j => !j.isValid)
-    if (possibleError.isEmpty) SCValidProof
+    if (possibleError.isEmpty) SCValidProof(proof)
     else possibleError.get
   }
 
diff --git a/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala b/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala
index cb030de9..0bb0cbc8 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.Helpers.{_, 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 6bd499c0..81b81922 100644
--- a/src/main/scala/lisa/settheory/SetTheoryTGAxioms.scala
+++ b/src/main/scala/lisa/settheory/SetTheoryTGAxioms.scala
@@ -1,6 +1,7 @@
 package lisa.settheory
+
 import lisa.kernel.fol.FOL._
-import utilities.KernelHelpers.{_, given}
+import utilities.Helpers.{_, 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 5a47aad9..11fde4e4 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.Helpers.{_, 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 13221cc1..e89ea065 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.Helpers.{_, 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 3d674ce8..331916cc 100644
--- a/src/main/scala/proven/DSetTheory/Part1.scala
+++ b/src/main/scala/proven/DSetTheory/Part1.scala
@@ -1,8 +1,5 @@
 package proven.DSetTheory
-import lisa.kernel.Printer
-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,8 +11,11 @@ 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 utilities.Helpers.{_, given}
+import utilities.Printer
+import utilities.Printer.prettyFormula
+import utilities.Printer.prettySCProof
+import utilities.Printer.prettySequent
 
 import scala.collection.immutable
 import scala.collection.immutable.SortedSet
@@ -397,8 +397,6 @@ object Part1 {
 
   /*
     val lemma2 = SCProof({
-
-
         // goal ∀b. (b ∈ ?B) ⇒ ∀a. (a ∈ ?A) ⇒ ∃!x. ?psi(x, a, b)   ⊢   ∃!Z. ∃X. Z=UX /\ ∀x. (x ∈ X) ↔ ∃b. (b ∈ ?B) ∧ ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ ?A) ∧ ?psi(x1, a, b)
         // redGoal ∀b. (b ∈ ?B) ⇒ ∀a. (a ∈ ?A) ⇒ ∃!x. ?psi(x, a, b)   ⊢   ∃Z1. ∀Z. Z=Z1 <=> ∃X. Z=UX /\ ∀x. (x ∈ X) ↔ ∃b. (b ∈ ?B) ∧ ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ ?A) ∧ ?psi(x1, a, b)
         // redGoal ∀b. (b ∈ ?B) ⇒ ∀a. (a ∈ ?A) ⇒ ∃!x. ?psi(x, a, b)   ⊢   ∀Z. Z=UX <=> ∃X. Z=UX /\ ∀x. (x ∈ X) ↔ ∃b. (b ∈ ?B) ∧ ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ ?A) ∧ ?psi(x1, a, b)
@@ -572,13 +570,10 @@ object Part1 {
   }
   /*
     val thm_lemmaCartesianProduct = theory.proofToTheorem("lemmaCartesianProduct", lemmaCartesianProduct, Seq(thm_lemmaMapTwoArguments)).get
-
     val vA = VariableLabel("A")
     val vB = VariableLabel("B")
     val cart_product = ConstantFunctionLabel("cart_cross", 2)
     val def_oPair = theory.makeFunctionDefinition(lemmaCartesianProduct, Seq(thm_lemmaMapTwoArguments), cart_product, Seq(vA, vB), VariableLabel("z"), innerOfDefinition(lemmaCartesianProduct.conclusion.right.head)).get
-
-
    */
 
   def innerOfDefinition(f: Formula): Formula = f match {
@@ -600,10 +595,7 @@ object Part1 {
   }
 
   def main(args: Array[String]): Unit = {
-    def checkProof(proof: SCProof): Unit = {
-      val error = SCProofChecker.checkSCProof(proof)
-      println(prettySCProof(proof, error))
-    }
+
     println("\nthmMapFunctional")
     checkProof(thmMapFunctional)
     println("\nlemma1")
diff --git a/src/main/scala/proven/ElementsOfSetTheory.scala b/src/main/scala/proven/ElementsOfSetTheory.scala
index c1fd97c4..e5c83222 100644
--- a/src/main/scala/proven/ElementsOfSetTheory.scala
+++ b/src/main/scala/proven/ElementsOfSetTheory.scala
@@ -1,20 +1,17 @@
 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 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 utilities.Helpers.{_, given}
+import utilities.Printer
+import utilities.Printer.*
 
 import scala.collection.immutable
 import scala.collection.immutable.SortedSet
@@ -72,7 +69,7 @@ object ElementsOfSetTheory {
     val fin4 = generalizeToForall(fin3, fin3.conclusion.right.head, y)
     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
 
@@ -324,7 +321,7 @@ object ElementsOfSetTheory {
     val p2 = RightImplies(emptySeq +> (p1.bot.left.head ==> p1.bot.right.head), 1, p1.bot.left.head, p1.bot.right.head) //   |- ({x,y}={x',y'}) ==> (x=x' /\ y=y')\/(x=y' /\ y=x')
     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",
@@ -342,7 +339,6 @@ object ElementsOfSetTheory {
 
   /*
   val proofOrderedPairDeconstruction: SCProof = {
-
     val opairxy = pair(pair(x, y), pair(x, x))
     val opairxx = pair(pair(x, x), pair(x, x))
     val opairxy1 = pair(pair(x1, y1), pair(x1, x1))
@@ -351,11 +347,8 @@ object ElementsOfSetTheory {
     val pairxx = pair(x, x)
     val pairxy1 = pair(x1, y1)
     val pairxx1 = pair(x1, x1)
-
-
     val p0 = SCSubproof(orderedPairDefinition, display = false)
     val p1 = SCSubproof(proofUnorderedPairDeconstruction) //  |- ∀∀∀∀(({x$4,y$3}={x'$2,y'$1})⇒(((y'$1=y$3)∧(x'$2=x$4))∨((x$4=y'$1)∧(y$3=x'$2))))
-
     val p2: SCSubproof = SCSubproof(SCProof(byCase(x === y)(
       {
         val p2_0 = SCSubproof(SCProof({
@@ -388,7 +381,6 @@ object ElementsOfSetTheory {
         }, IndexedSeq(-2)) //   {x',y'}={x,x}, x=y |- x=x' /\ x=y'
         val p2_2 = Cut(emptySeq ++< p2_0.bot ++> p2_1.bot, 0, 1, p2_0.bot.right.head) //   ((x,y)=(x',y')), x=y |- x=x' /\ x=y'
         val p2_3 = RightSubstEq(emptySeq +< (oPair(x, y) === oPair(x1, y1)) +< (x === y) +> ((x === x1) /\ (y === y1)), 2, x, y, (x === x1) /\ (z === y1), z)
-
         SCSubproof(SCProof(IndexedSeq(p2_0, p2_1, p2_2, p2_3), IndexedSeq(p0, p1)), IndexedSeq(-1, -2))
       } //   ((x,y)=(x',y')), x=y |- x=x' /\ y=y'
       ,
@@ -398,10 +390,8 @@ object ElementsOfSetTheory {
           val p2_0_1 = UseFunctionDefinition(emptySeq +> (oPair(x1, y1) === opairxy1), oPair, Seq(x1, y1)) // |- (x1, y1) === {{x1,y1}, {x1,x1}}
           val p2_0_2 = RightSubstEq(emptySeq +< (oPair(x, y) === oPair(x1, y1)) +> (oPair(x1, y1) === pair(pair(x, y), pair(x, x))),
             0, oPair(x, y), oPair(x1, y1), z === pair(pair(x, y), pair(x, x)), z) //  (x1,y1)=(x,y) |- ((x1,y1)={{x,y},{x,x}})
-
           val p2_0_3 = RightSubstEq(emptySeq +< (oPair(x, y) === oPair(x1, y1)) +< (opairxy1 === oPair(x1, y1)) +> (pair(pair(x, y), pair(x, x)) === pair(pair(x1, y1), pair(x1, x1))),
             2, opairxy1, oPair(x1, y1), z === pair(pair(x, y), pair(x, x)), z) //  (x1,y1)=(x,y), (x1,y1)={{x1,y1}, {x1,x1}} |- {{x1,y1}, {x1,x1}}={{x,y},{x,x}})
-
           val p2_0_4 = Cut(emptySeq +< (oPair(x, y) === oPair(x1, y1)) +> (pair(pair(x, y), pair(x, x)) === pair(pair(x1, y1), pair(x1, x1))),
             1, 3, opairxy1 === oPair(x1, y1))
           SCProof(IndexedSeq(p2_0_0, p2_0_1, p2_0_2, p2_0_3, p2_0_4), IndexedSeq(p0))
@@ -414,7 +404,6 @@ object ElementsOfSetTheory {
           case BinaryConnectorFormula(`or`, l, r) => (l, r)
         }
         val pr2_1: SCProof = destructRightOr(pr2_0, f, g) // ((x,y)=(x',y')) |- (({x',x'}={x,y})∧({x',y'}={x,x})), (({x,x}={x',x'})∧({x,y}={x',y'}))
-
         val pb2_0 = SCSubproof({
           val prb2_0_0 = instantiateForall(SCProof(IndexedSeq(), IndexedSeq(p1)), x, y, x1, x1) //  |- (({x,y}={x',x'}) ⇒ (((x'=y)∧(x'=x))∨((x=x')∧(y=x'))))
           val f = (x1 === y) /\ (x1 === x)
@@ -427,10 +416,8 @@ object ElementsOfSetTheory {
           SCProof(IndexedSeq(pb3_0_0, pb3_0_1, pb3_0_2, pb3_0_3, pb3_0_4), IndexedSeq(p1))
         }, IndexedSeq(-2)) // {x',x'}={x,y} |- x=y
         val pb2_1 = SCSubproof(destructRightAnd(pr2_1, pairxx1 === pairxy, pairxx === pairxy1), IndexedSeq(-1, -2)) // ((x,y)=(x',y')) |- (({x',x'}={x,y}), (({x,x}={x',x'})∧({x,y}={x',y'}))
-
         val pb2_2 = Cut(pb2_1.bot -> pb2_0.bot.left.head +> (x === y), 1, 0, pb2_0.bot.left.head) // ((x,y)=(x',y')) |- x=y, (({x,x}={x',x'})∧({x,y}={x',y'}))
         val pc2_0 = SCSubproof(SCProof(IndexedSeq(pb2_0, pb2_1, pb2_2), IndexedSeq(p0, p1)), IndexedSeq(-1, -2)) // ((x,y)=(x',y')) |- x=y, (({x,x}={x',x'})∧({x,y}={x',y'}))
-
         val pc2_1 = SCSubproof({
           val pc2_1_0 = SCSubproof(destructRightAnd(SCProof(IndexedSeq(), IndexedSeq(pc2_0)), pairxy === pairxy1, pairxx === pairxx1), IndexedSeq(-2)) // ((x,y)=(x',y')) |- x=y, {x,y}={x',y'}
           val pc2_1_1 = SCSubproof(instantiateForall(SCProof(IndexedSeq(), IndexedSeq(p1)), x, y, x1, y1), IndexedSeq(-1)) //   (({x,y}={x',y'})⇒(((y'=y)∧(x'=x))∨((x=y')∧(y=x'))))
@@ -450,7 +437,6 @@ object ElementsOfSetTheory {
           val prc2_2_4 = destructRightAnd(prc2_2_3, x === x1, x === x1) // ((x,y)=(x',y')) |- x=y, x'=x
           SCProof(prc2_2_4.steps, IndexedSeq(p1, pc2_0))
         }, IndexedSeq(-2, 0)) // ((x,y)=(x',y')) |- x=y, x'=x
-
         val pc2_3 = RightSubstEq(pc2_1.bot -> (x1 === y) +> (x === y) +< (x1 === x), 1, x, x1, z === y, z) // ((x,y)=(x',y')), x=x' |- x=y, ((y=y')∧(x=x')))
         val pc2_4 = Cut(pc2_3.bot -< (x === x1), 2, 3, x === x1) // ((x,y)=(x',y')) |- x=y, ((y=y')∧(x=x')))
         val pc2_5 = LeftNot(pc2_4.bot +< !(x === y) -> (x === y), 4, x === y) // ((x,y)=(x',y')), !x=y |-  ((y=y')∧(x=x')))
@@ -458,16 +444,12 @@ object ElementsOfSetTheory {
       } //   ((x,y)=(x',y')), !x=y |- x=x' /\ y=y'
     ).steps, IndexedSeq(p0, p1)), IndexedSeq(0, 1)) //   ((x,y)=(x',y')) |- x=x' /\ y=y'
     SCProof(p0, p1, p2)
-
     ???
   } // |- (x,y)=(x', y')  ===>  x=x' /\ y=y'
    */
 
   def main(args: Array[String]): Unit = {
-    def checkProof(proof: SCProof): Unit = {
-      val error = SCProofChecker.checkSCProof(proof)
-      println(prettySCProof(proof, error))
-    }
+
     println("\nproofUnorderedPairSymmetry")
     checkProof(proofUnorderedPairSymmetry)
     println("\nproofUnorderedPairDeconstruction")
diff --git a/src/main/scala/proven/tactics/Destructors.scala b/src/main/scala/proven/tactics/Destructors.scala
index 86fdd967..39f2c6cd 100644
--- a/src/main/scala/proven/tactics/Destructors.scala
+++ b/src/main/scala/proven/tactics/Destructors.scala
@@ -5,7 +5,7 @@ import lisa.kernel.proof.SCProof
 import lisa.kernel.proof.SequentCalculus.*
 import lisa.kernel.proof.SequentCalculus.*
 import proven.tactics.ProofTactics.hypothesis
-import utilities.KernelHelpers.*
+import utilities.Helpers.*
 
 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 50b4d61a..5ac98af4 100644
--- a/src/main/scala/proven/tactics/ProofTactics.scala
+++ b/src/main/scala/proven/tactics/ProofTactics.scala
@@ -1,10 +1,10 @@
 package proven.tactics
 
-import lisa.kernel.Printer.*
 import lisa.kernel.fol.FOL.*
 import lisa.kernel.proof.SCProof
 import lisa.kernel.proof.SequentCalculus.*
-import utilities.KernelHelpers.{_, given}
+import utilities.Helpers.{_, given}
+import utilities.Printer.*
 
 import scala.collection.immutable.Set
 
diff --git a/src/main/scala/proven/tactics/SimplePropositionalSolver.scala b/src/main/scala/proven/tactics/SimplePropositionalSolver.scala
index a48c558f..69e75d73 100644
--- a/src/main/scala/proven/tactics/SimplePropositionalSolver.scala
+++ b/src/main/scala/proven/tactics/SimplePropositionalSolver.scala
@@ -3,7 +3,7 @@ package proven.tactics
 import lisa.kernel.fol.FOL.*
 import lisa.kernel.proof.SCProof
 import lisa.kernel.proof.SequentCalculus.*
-import utilities.KernelHelpers.*
+import utilities.Helpers.*
 
 import scala.collection.mutable.Set as mSet
 
diff --git a/src/main/scala/utilities/KernelHelpers.scala b/src/main/scala/utilities/KernelHelpers.scala
index 2e7ac736..f9967ba8 100644
--- a/src/main/scala/utilities/KernelHelpers.scala
+++ b/src/main/scala/utilities/KernelHelpers.scala
@@ -14,7 +14,7 @@ import lisa.kernel.proof.SequentCalculus.isSameSequent
  * import lisa.KernelHelpers.*
  * </pre>
  */
-object KernelHelpers {
+trait KernelHelpers {
 
   import lisa.kernel.fol.FOL.*
   import lisa.kernel.proof.SequentCalculus.Sequent
diff --git a/src/main/scala/utilities/TheoriesHelpers.scala b/src/main/scala/utilities/TheoriesHelpers.scala
index e0f9864e..9d6c32d2 100644
--- a/src/main/scala/utilities/TheoriesHelpers.scala
+++ b/src/main/scala/utilities/TheoriesHelpers.scala
@@ -1,13 +1,12 @@
 package utilities
 
-import lisa.kernel.proof.RunningTheory
-import lisa.kernel.proof.RunningTheoryJudgement
+import lisa.kernel.fol.FOL.*
 import lisa.kernel.proof.RunningTheoryJudgement.InvalidJustification
-import lisa.kernel.proof.SCProof
-import lisa.kernel.proof.SequentCalculus.Rewrite
-import lisa.kernel.proof.SequentCalculus.isSameSequent
+import lisa.kernel.proof.SequentCalculus.*
+import lisa.kernel.proof.*
+import utilities.Printer
 
-object TheoriesHelpers {
+trait TheoriesHelpers extends KernelHelpers {
 
   // for when the kernel will have a dedicated parser
   extension (theory: RunningTheory)
@@ -18,4 +17,39 @@ object TheoriesHelpers {
       else InvalidJustification("The proof does not prove the claimed statement", None)
     }
 
+  extension (just: RunningTheory#Justification)
+    def show(output: String => Unit = println): just.type = {
+      just match
+        case thm: RunningTheory#Theorem => output(s"Theorem ${thm.name} := ${Printer.prettySequent(thm.proposition)}")
+        case axiom: RunningTheory#Axiom => output(s"Axiom ${axiom.name} := ${Printer.prettyFormula(axiom.ax)}")
+        case d: RunningTheory#Definition =>
+          d match
+            case pd: RunningTheory#PredicateDefinition =>
+              output(s"Definition of predicate symbol ${pd.label.id} := ${Printer.prettyFormula(pd.label(pd.args.map(VariableTerm(_))*) <=> pd.phi)}") // (label, args, phi)
+            case fd: RunningTheory#FunctionDefinition =>
+              output(s"Definition of function symbol ${fd.label.id} := ${Printer.prettyFormula((fd.label(fd.args.map(VariableTerm(_))*) === fd.out) <=> fd.phi)})")
+        // output(Printer.prettySequent(thm.proposition))
+        // thm
+      just
+    }
+
+  extension [J <: RunningTheory#Justification](theoryJudgement: RunningTheoryJudgement[J]) {
+
+    def showAndGet(output: String => Unit = println): J = {
+      theoryJudgement match
+        case RunningTheoryJudgement.ValidJustification(just) =>
+          just.show(output)
+        case InvalidJustification(message, error) =>
+          output(s"$message\n${error match
+              case Some(judgement) => Printer.prettySCProof(judgement)
+              case None => ""
+            }")
+          theoryJudgement.get
+    }
+  }
+
+  def checkProof(proof: SCProof, output: String => Unit = println): Unit = {
+    val judgement = SCProofChecker.checkSCProof(proof)
+    output(Printer.prettySCProof(judgement))
+  }
 }
diff --git a/src/main/scala/utilities/tptp/KernelParser.scala b/src/main/scala/utilities/tptp/KernelParser.scala
index 3f7d2fe0..215e85d7 100644
--- a/src/main/scala/utilities/tptp/KernelParser.scala
+++ b/src/main/scala/utilities/tptp/KernelParser.scala
@@ -6,7 +6,7 @@ import leo.datastructures.TPTP.FOF
 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.Helpers.*
 import utilities.tptp.*
 
 import java.io.File
diff --git a/src/test/scala/lisa/kernel/EquivalenceCheckerTests.scala b/src/test/scala/lisa/kernel/EquivalenceCheckerTests.scala
index 2576c9c9..c499619e 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 lisa.kernel.Printer
+import utilities.Printer
 import lisa.kernel.fol.FOL
 import lisa.kernel.fol.FOL.*
 import org.scalatest.funsuite.AnyFunSuite
-import utilities.KernelHelpers.*
+import utilities.Helpers.*
 
 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 7ebe445c..42e6caed 100644
--- a/src/test/scala/lisa/kernel/FolTests.scala
+++ b/src/test/scala/lisa/kernel/FolTests.scala
@@ -1,6 +1,6 @@
 package lisa.kernel
 
-import lisa.kernel.Printer
+import utilities.Printer
 import lisa.kernel.fol.FOL.*
 import lisa.kernel.proof.RunningTheory
 import lisa.kernel.proof.RunningTheory.*
@@ -8,7 +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 utilities.Helpers.{_, 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 840dbd5d..3d7aa18b 100644
--- a/src/test/scala/lisa/kernel/IncorrectProofsTests.scala
+++ b/src/test/scala/lisa/kernel/IncorrectProofsTests.scala
@@ -5,7 +5,7 @@ import lisa.kernel.fol.FOL.*
 import lisa.kernel.proof.SCProof
 import lisa.kernel.proof.SequentCalculus.*
 import test.ProofCheckerSuite
-import utilities.KernelHelpers.*
+import utilities.Helpers.*
 
 import scala.collection.immutable.SortedSet
 import scala.language.implicitConversions
diff --git a/src/test/scala/lisa/kernel/PrinterTest.scala b/src/test/scala/lisa/kernel/PrinterTest.scala
index cf6a4899..67e91f29 100644
--- a/src/test/scala/lisa/kernel/PrinterTest.scala
+++ b/src/test/scala/lisa/kernel/PrinterTest.scala
@@ -1,6 +1,6 @@
 package lisa.kernel
 
-import lisa.kernel.Printer._
+import utilities.Printer._
 import lisa.kernel.fol.FOL._
 import org.scalatest.funsuite.AnyFunSuite
 
diff --git a/src/test/scala/lisa/kernel/ProofTests.scala b/src/test/scala/lisa/kernel/ProofTests.scala
index fc559c9a..d5704b08 100644
--- a/src/test/scala/lisa/kernel/ProofTests.scala
+++ b/src/test/scala/lisa/kernel/ProofTests.scala
@@ -1,6 +1,6 @@
 package lisa.kernel
 
-import lisa.kernel.Printer
+import utilities.Printer
 import lisa.kernel.fol.FOL.*
 import lisa.kernel.proof.RunningTheory
 import lisa.kernel.proof.RunningTheory.*
@@ -8,7 +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 utilities.Helpers.{_, given}
 
 import scala.util.Random
 
diff --git a/src/test/scala/lisa/proven/ElementsOfSetTheoryTests.scala b/src/test/scala/lisa/proven/ElementsOfSetTheoryTests.scala
index b9e09182..36a3fb11 100644
--- a/src/test/scala/lisa/proven/ElementsOfSetTheoryTests.scala
+++ b/src/test/scala/lisa/proven/ElementsOfSetTheoryTests.scala
@@ -1,6 +1,6 @@
-package proven
+package lisa.proven
 
-import lisa.kernel.Printer
+import utilities.Printer
 import lisa.kernel.fol.FOL.*
 import lisa.kernel.fol.FOL.*
 import lisa.kernel.proof.SCProof
@@ -10,8 +10,8 @@ import lisa.settheory.AxiomaticSetTheory.*
 import proven.ElementsOfSetTheory.*
 import proven.tactics.ProofTactics
 import test.ProofCheckerSuite
-import utilities.KernelHelpers.{_, given}
-import utilities.KernelHelpers.{_, given}
+import utilities.Helpers.{_, given}
+import utilities.Helpers.{_, given}
 
 class ElementsOfSetTheoryTests extends ProofCheckerSuite {
 
diff --git a/src/test/scala/lisa/proven/SimpleProverTests.scala b/src/test/scala/lisa/proven/SimpleProverTests.scala
index e0b99c73..8598562a 100644
--- a/src/test/scala/lisa/proven/SimpleProverTests.scala
+++ b/src/test/scala/lisa/proven/SimpleProverTests.scala
@@ -1,14 +1,14 @@
-package proven
+package lisa.proven
 
-import lisa.kernel.Printer
-import lisa.kernel.Printer.*
+import utilities.Printer
+import utilities.Printer.*
 import lisa.kernel.fol.FOL.*
 import lisa.kernel.proof.RunningTheory
 import lisa.kernel.proof.RunningTheory.PredicateLogic
 import lisa.kernel.proof.SCProofChecker
 import org.scalatest.funsuite.AnyFunSuite
 import proven.tactics.SimplePropositionalSolver as SPS
-import utilities.KernelHelpers.*
+import utilities.Helpers.*
 import utilities.tptp.KernelParser.*
 import utilities.tptp.ProblemGatherer.getPRPproblems
 
diff --git a/src/test/scala/test/ProofCheckerSuite.scala b/src/test/scala/test/ProofCheckerSuite.scala
index 8a6011d7..caaee39f 100644
--- a/src/test/scala/test/ProofCheckerSuite.scala
+++ b/src/test/scala/test/ProofCheckerSuite.scala
@@ -1,14 +1,14 @@
 package test
 
-import lisa.kernel.Printer
+import utilities.Printer
 import lisa.kernel.proof.SCProof
 import lisa.kernel.proof.SCProofChecker._
 import lisa.kernel.proof.SequentCalculus.Sequent
 import lisa.kernel.proof.SequentCalculus.isSameSequent
 import lisa.settheory.AxiomaticSetTheory
 import org.scalatest.funsuite.AnyFunSuite
-import utilities.KernelHelpers._
-import utilities.KernelHelpers.given_Conversion_Boolean_List_String_Option
+import utilities.Helpers._
+import utilities.Helpers.given_Conversion_Boolean_List_String_Option
 
 abstract class ProofCheckerSuite extends AnyFunSuite {
   import lisa.kernel.fol.FOL.*
@@ -39,14 +39,14 @@ abstract class ProofCheckerSuite extends AnyFunSuite {
 
   val axioms = AxiomaticSetTheory.axioms
   def checkProof(proof: SCProof): Unit = {
-    val error = checkSCProof(proof)
-    println(Printer.prettySCProof(proof, error))
+    val judgement = checkSCProof(proof)
+    println(Printer.prettySCProof(judgement))
     println(s"\n(${proof.totalLength} proof steps in total)")
   }
 
   def checkProof(proof: SCProof, expected: Sequent): Unit = {
     val judgement = checkSCProof(proof)
-    assert(judgement.isValid, "\n" + Printer.prettySCProof(proof, judgement))
+    assert(judgement.isValid, "\n" + Printer.prettySCProof( judgement))
     assert(isSameSequent(proof.conclusion, expected), s"(${Printer.prettySequent(proof.conclusion)} did not equal ${Printer.prettySequent(expected)})")
   }
 
-- 
GitLab