diff --git a/build.sbt b/build.sbt
index 83ed470471b59224285360ccdcf5cbdb9dd6ca55..06d0a3121182945da4980a569c20fd3818833538 100644
--- a/build.sbt
+++ b/build.sbt
@@ -37,7 +37,7 @@ def withTests(project: Project): ClasspathDependency =
 
 lazy val root = Project(
   id = "lisa",
-  base = file("lisa"),
+  base = file("."),
 )
   .settings(commonSettings3)
   .settings(
diff --git a/lisa-examples/src/main/scala/Example.scala b/lisa-examples/src/main/scala/Example.scala
index 725ef41013259f46aad268696faa807b322f68f0..85e4592822b8eeeafaddd0f8bad3d4ef9adae13f 100644
--- a/lisa-examples/src/main/scala/Example.scala
+++ b/lisa-examples/src/main/scala/Example.scala
@@ -15,7 +15,7 @@ import lisa.utils.Printer.*
  */
 object Example {
   def main(args: Array[String]): Unit = {
-    proofExample() // uncomment when exercise finished
+    //proofExample() // uncomment when exercise finished
     // solverExample()
     // tptpExample()
   }
diff --git a/lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaDefinitions.scala b/lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaDefinitions.scala
index 7f5d40447619e83173f5ce7be66c891c29cde375..0a19f26084ffd3a4912fbe5964c6ba85743cb7b8 100644
--- a/lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaDefinitions.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaDefinitions.scala
@@ -22,7 +22,7 @@ private[fol] trait FormulaDefinitions extends FormulaLabelDefinitions with TermD
   /**
    * The formula counterpart of [[PredicateLabel]].
    */
-  final case class PredicateFormula(label: PredicateLabel, args: Seq[Term]) extends Formula {
+  sealed case class PredicateFormula(label: PredicateLabel, args: Seq[Term]) extends Formula {
     override def freeVariables: Set[VariableLabel] = args.foldLeft(Set.empty[VariableLabel])((prev, next) => prev union next.freeVariables)
 
     override def constantPredicates: Set[ConstantPredicateLabel] = label match {
@@ -41,7 +41,7 @@ private[fol] trait FormulaDefinitions extends FormulaLabelDefinitions with TermD
   /**
    * The formula counterpart of [[ConnectorLabel]].
    */
-  final case class ConnectorFormula(label: ConnectorLabel, args: Seq[Formula]) extends Formula {
+  sealed case class ConnectorFormula(label: ConnectorLabel, args: Seq[Formula]) extends Formula {
     override def freeVariables: Set[VariableLabel] = args.foldLeft(Set.empty[VariableLabel])((prev, next) => prev union next.freeVariables)
 
     override def constantFunctions: Set[ConstantFunctionLabel] = args.foldLeft(Set.empty[ConstantFunctionLabel])((prev, next) => prev union next.constantFunctions)
@@ -54,7 +54,7 @@ private[fol] trait FormulaDefinitions extends FormulaLabelDefinitions with TermD
   /**
    * The formula counterpart of [[BinderLabel]].
    */
-  final case class BinderFormula(label: BinderLabel, bound: VariableLabel, inner: Formula) extends Formula {
+  sealed case class BinderFormula(label: BinderLabel, bound: VariableLabel, inner: Formula) extends Formula {
     override def freeVariables: Set[VariableLabel] = inner.freeVariables - bound
 
     override def constantFunctions: Set[ConstantFunctionLabel] = inner.constantFunctions
diff --git a/lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaLabelDefinitions.scala b/lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaLabelDefinitions.scala
index 28b6c86946953303643d4a45dc1e360dca7de3a0..b1d14331fd7cf0c906c45f4335b8073d6b6e6cee 100644
--- a/lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaLabelDefinitions.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaLabelDefinitions.scala
@@ -41,7 +41,7 @@ private[fol] trait FormulaLabelDefinitions extends CommonDefinitions {
   /**
    * A standard predicate symbol. Typical example are equality (=) and membership (∈)
    */
-  final case class ConstantPredicateLabel(id: String, arity: Int) extends PredicateLabel with ConstantLabel
+  sealed case class ConstantPredicateLabel(id: String, arity: Int) extends PredicateLabel with ConstantLabel
 
   /**
    * The equality symbol (=) for first order logic.
@@ -51,7 +51,7 @@ private[fol] trait FormulaLabelDefinitions extends CommonDefinitions {
   /**
    * A predicate symbol that can be instantiated with any formula.
    */
-  final case class SchematicPredicateLabel(id: String, arity: Int) extends PredicateLabel
+  sealed case class SchematicPredicateLabel(id: String, arity: Int) extends PredicateLabel
 
   /**
    * The label for a connector, namely a function taking a fixed number of formulas and returning another formula.
diff --git a/lisa-kernel/src/main/scala/lisa/kernel/fol/TermDefinitions.scala b/lisa-kernel/src/main/scala/lisa/kernel/fol/TermDefinitions.scala
index 3a01b5eaf468d1130be5f262319c9f647976c3f9..e98ca824e4da99f615811a391b3c53556b8908a4 100644
--- a/lisa-kernel/src/main/scala/lisa/kernel/fol/TermDefinitions.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/fol/TermDefinitions.scala
@@ -26,7 +26,7 @@ private[fol] trait TermDefinitions extends TermLabelDefinitions {
    *
    * @param label The label of the variable.
    */
-  final case class VariableTerm(label: VariableLabel) extends Term {
+  sealed case class VariableTerm(label: VariableLabel) extends Term {
     override def freeVariables: Set[VariableLabel] = Set(label)
 
     override def constantFunctions: Set[ConstantFunctionLabel] = Set.empty
@@ -39,7 +39,7 @@ private[fol] trait TermDefinitions extends TermLabelDefinitions {
    * @param label The label of the node
    * @param args  children of the node. The number of argument must be equal to the arity of the function.
    */
-  final case class FunctionTerm(label: FunctionLabel, args: Seq[Term]) extends Term {
+  sealed case class FunctionTerm(label: FunctionLabel, args: Seq[Term]) extends Term {
     require(label.arity == args.size)
 
     override def freeVariables: Set[VariableLabel] = args.foldLeft(Set.empty[VariableLabel])((prev, next) => prev union next.freeVariables)
diff --git a/lisa-kernel/src/main/scala/lisa/kernel/fol/TermLabelDefinitions.scala b/lisa-kernel/src/main/scala/lisa/kernel/fol/TermLabelDefinitions.scala
index 4d36c24773ff392cd97dbf2036f8997856f52bc0..c2691946010a4332bf45db3716e58305d75aaf5b 100644
--- a/lisa-kernel/src/main/scala/lisa/kernel/fol/TermLabelDefinitions.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/fol/TermLabelDefinitions.scala
@@ -34,7 +34,7 @@ private[fol] trait TermLabelDefinitions extends CommonDefinitions {
    *
    * @param id The name of the variable, for example "x" or "y".
    */
-  final case class VariableLabel(id: String) extends TermLabel {
+  sealed case class VariableLabel(id: String) extends TermLabel {
     val name: String = id
   }
 
@@ -54,7 +54,7 @@ private[fol] trait TermLabelDefinitions extends CommonDefinitions {
    * @param id    The name of the function symbol.
    * @param arity The arity of the function symbol. A function symbol of arity 0 is a constant
    */
-  final case class ConstantFunctionLabel(id: String, arity: Int) extends FunctionLabel with ConstantLabel
+  sealed case class ConstantFunctionLabel(id: String, arity: Int) extends FunctionLabel with ConstantLabel
 
   /**
    * A schematic function symbol that can be substituted.
@@ -62,7 +62,7 @@ private[fol] trait TermLabelDefinitions extends CommonDefinitions {
    * @param id    The name of the function symbol.
    * @param arity The arity of the function symbol. A function symbol of arity 0 is a constant
    */
-  final case class SchematicFunctionLabel(id: String, arity: Int) extends FunctionLabel
+  sealed case class SchematicFunctionLabel(id: String, arity: Int) extends FunctionLabel
 
   /**
    * A function returning true if and only if the two symbols are considered "the same".
diff --git a/lisa-kernel/src/main/scala/lisa/kernel/proof/RunningTheory.scala b/lisa-kernel/src/main/scala/lisa/kernel/proof/RunningTheory.scala
index 7d15e8e5603893c24b154874f4834784cc692c94..ce544cf2be2997754b29dcb4de9129f8fa2b3be7 100644
--- a/lisa-kernel/src/main/scala/lisa/kernel/proof/RunningTheory.scala
+++ b/lisa-kernel/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
+  sealed 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
+  sealed case class Axiom private[RunningTheory] (name: String, ax: Formula) extends Justification
 
   /**
    * A definition can be either a PredicateDefinition or a FunctionDefinition.
@@ -47,7 +47,7 @@ class RunningTheory {
    * @param label The name and arity of the new symbol
    * @param expression The formula, depending on terms, that define the symbol.
    */
-  final case class PredicateDefinition private[RunningTheory] (label: ConstantPredicateLabel, expression: LambdaTermFormula) extends Definition
+  sealed case class PredicateDefinition private[RunningTheory] (label: ConstantPredicateLabel, expression: LambdaTermFormula) extends Definition
 
   /**
    * Define a function symbol as the unique element that has some property. The existence and uniqueness
@@ -58,7 +58,7 @@ class RunningTheory {
    * @param out   The variable representing the result of the function in phi
    * @param expression   The formula, with term parameters, defining the function.
    */
-  final case class FunctionDefinition private[RunningTheory] (label: ConstantFunctionLabel, out: VariableLabel, expression: LambdaTermFormula) extends Definition
+  sealed case class FunctionDefinition private[RunningTheory] (label: ConstantFunctionLabel, out: VariableLabel, expression: LambdaTermFormula) extends Definition
 
   private[proof] val theoryAxioms: mMap[String, Axiom] = mMap.empty
   private[proof] val theorems: mMap[String, Theorem] = mMap.empty
diff --git a/lisa/src/main/scala/lisa/proven/Main.scala b/src/main/scala/lisa/proven/Main.scala
similarity index 100%
rename from lisa/src/main/scala/lisa/proven/Main.scala
rename to src/main/scala/lisa/proven/Main.scala
diff --git a/lisa/src/main/scala/lisa/proven/SetTheoryLibrary.scala b/src/main/scala/lisa/proven/SetTheoryLibrary.scala
similarity index 100%
rename from lisa/src/main/scala/lisa/proven/SetTheoryLibrary.scala
rename to src/main/scala/lisa/proven/SetTheoryLibrary.scala
diff --git a/lisa/src/main/scala/lisa/proven/mathematics/Mapping.scala b/src/main/scala/lisa/proven/mathematics/Mapping.scala
similarity index 100%
rename from lisa/src/main/scala/lisa/proven/mathematics/Mapping.scala
rename to src/main/scala/lisa/proven/mathematics/Mapping.scala
diff --git a/lisa/src/main/scala/lisa/proven/mathematics/SetTheory.scala b/src/main/scala/lisa/proven/mathematics/SetTheory.scala
similarity index 100%
rename from lisa/src/main/scala/lisa/proven/mathematics/SetTheory.scala
rename to src/main/scala/lisa/proven/mathematics/SetTheory.scala
diff --git a/lisa/src/main/scala/lisa/proven/tactics/Destructors.scala b/src/main/scala/lisa/proven/tactics/Destructors.scala
similarity index 100%
rename from lisa/src/main/scala/lisa/proven/tactics/Destructors.scala
rename to src/main/scala/lisa/proven/tactics/Destructors.scala
diff --git a/lisa/src/main/scala/lisa/proven/tactics/ProofTactics.scala b/src/main/scala/lisa/proven/tactics/ProofTactics.scala
similarity index 100%
rename from lisa/src/main/scala/lisa/proven/tactics/ProofTactics.scala
rename to src/main/scala/lisa/proven/tactics/ProofTactics.scala
diff --git a/lisa/src/main/scala/lisa/proven/tactics/SimplePropositionalSolver.scala b/src/main/scala/lisa/proven/tactics/SimplePropositionalSolver.scala
similarity index 100%
rename from lisa/src/main/scala/lisa/proven/tactics/SimplePropositionalSolver.scala
rename to src/main/scala/lisa/proven/tactics/SimplePropositionalSolver.scala
diff --git a/lisa/src/test/scala/lisa/proven/InitialProofsTests.scala b/src/test/scala/lisa/proven/InitialProofsTests.scala
similarity index 100%
rename from lisa/src/test/scala/lisa/proven/InitialProofsTests.scala
rename to src/test/scala/lisa/proven/InitialProofsTests.scala
diff --git a/lisa/src/test/scala/lisa/proven/SimpleProverTests.scala b/src/test/scala/lisa/proven/SimpleProverTests.scala
similarity index 100%
rename from lisa/src/test/scala/lisa/proven/SimpleProverTests.scala
rename to src/test/scala/lisa/proven/SimpleProverTests.scala