diff --git a/Reference Manual/lisa.pdf b/Reference Manual/lisa.pdf
index 0bb3bc56b7a4198c5b8b355aacb861ce96cfcf9e..eaf56b7b5c01b55cc12b6f2af64db6b51935ed3d 100644
Binary files a/Reference Manual/lisa.pdf and b/Reference Manual/lisa.pdf differ
diff --git a/Reference Manual/macro.tex b/Reference Manual/macro.tex
index bc2077294385c754cb7a040c26095609ab24cbcd..f0aa42bfb88ef3e1c8e2f0da60849bab164a884f 100644
--- a/Reference Manual/macro.tex	
+++ b/Reference Manual/macro.tex	
@@ -109,6 +109,7 @@
     extendedchars = true,
     inputencoding = utf8,
     alsoletter={@,=,>},
+    backgroundcolor = \color{rosishlightgray},
     keywordstyle = {\color{blue}},
     keywordstyle = [2]{\color{blue}},
     commentstyle = \color{comments},
@@ -132,6 +133,7 @@
     extendedchars = true,
     inputencoding = utf8,
     alsoletter={@,=,>},
+    backgroundcolor = \color{rosishlightgray},
     keywordstyle = {\color{blue}},
     keywordstyle = [2]{\color{blue}},
     keywordstyle = [3]{\color{green}},
@@ -175,7 +177,6 @@
     extendedchars = true,
     inputencoding = utf8,
     extendedchars = \true,
-    backgroundcolor = \color{rosishlightgray},
     basicstyle=\footnotesize\linespread{1.15}\ttfamily,
     mathescape,
     escapeinside={!*}{*!},
diff --git a/build.sbt b/build.sbt
index 4040147ac2ae098a0e5b73f5808e361cced63132..fe70063a55ffa798d09509892a879a05f98ecc33 100644
--- a/build.sbt
+++ b/build.sbt
@@ -45,7 +45,8 @@ val commonSettings3 = Seq(
   ),
   libraryDependencies += "org.scalatest" %% "scalatest" % "3.2.10" % "test",
   libraryDependencies += "com.lihaoyi" %% "sourcecode" % "0.3.0",
-  libraryDependencies += "org.scala-lang.modules" %% "scala-parser-combinators" % "2.1.1",
+  //libraryDependencies += "org.scala-lang.modules" %% "scala-parser-combinators" % "2.1.1",
+  libraryDependencies += ("io.github.uuverifiers" %% "princess" % "2023-06-19").cross(CrossVersion.for3Use2_13),
   Test / parallelExecution := false
 )
 
@@ -56,6 +57,8 @@ def githubProject(repo: String, commitHash: String) = RootProject(uri(s"$repo#$c
 
 lazy val scallion = githubProject("https://github.com/sankalpgambhir/scallion.git", "6434e21bd08872cf547c8f0efb67c963bfdf4190")
 lazy val silex = githubProject("https://github.com/epfl-lara/silex.git", "fc07a8670a5fa8ea2dd5649a00424710274a5d18")
+// lazy val princess = RootProject(file("../princess")) // If you have a local copy of Princess and would like to do some changes
+//lazy val princess = githubProject("https://github.com/uuverifiers/princess.git", "93cbff11d7b02903e532c7b64207bc12f19b79c7")
 
 lazy val root = Project(
     id = "lisa",
@@ -66,7 +69,7 @@ lazy val root = Project(
     version := "0.1"
   )
   .dependsOn(kernel, withTests(utils)) // Everything but `examples`
-  .aggregate(kernel, utils) // To run tests on all modules
+  .aggregate(utils) // To run tests on all modules
 
 lazy val kernel = Project(
   id = "lisa-kernel",
diff --git a/lisa-examples/src/main/scala/Example.scala b/lisa-examples/src/main/scala/Example.scala
index 63c3d2b33eb436b93c6f5c3e63c09c61ed476f32..3e504167f400f5debc479ebd2d3e626a653c5e51 100644
--- a/lisa-examples/src/main/scala/Example.scala
+++ b/lisa-examples/src/main/scala/Example.scala
@@ -2,6 +2,8 @@ import lisa.prooflib.Substitution.{ApplyRules as Substitute}
 
 object Example extends lisa.Main {
 
+
+
   val x = variable
   val y = variable
   val P = predicate[1]
diff --git a/lisa-examples/src/main/scala/MapProofDef.scala b/lisa-examples/src/main/scala/MapProofDef.scala
deleted file mode 100644
index e91dfb0b4f70f844aed51995eee96877672f8c4f..0000000000000000000000000000000000000000
--- a/lisa-examples/src/main/scala/MapProofDef.scala
+++ /dev/null
@@ -1,106 +0,0 @@
-import lisa.automation.kernel.OLPropositionalSolver.*
-import lisa.automation.kernel.SimpleSimplifier.*
-import lisa.prooflib.BasicStepTactic.*
-import lisa.prooflib.ProofTacticLib.*
-import lisa.utils.FOLPrinter.*
-import lisa.utils.KernelHelpers.checkProof
-import lisa.utils.parsing.FOLPrinter
-import lisa.utils.unification.UnificationUtils.*
-
-object MapProofDef extends lisa.Main {
-  /*
-  val self = this
-
-  val x = variable
-  val y = variable
-  val xs = variable
-  val ys = variable
-  val f = variable
-
-
-
-  val Nil = ConstantFunctionLabel("Nil", 0)()
-  theory.addSymbol(ConstantFunctionLabel("Nil", 0))
-  val Cons = ConstantFunctionLabel("Cons", 2)
-  theory.addSymbol(Cons)
-
-  class TermProxy(t1:Term) {
-    infix def ::(t2: Term) = Cons(t2, t1)
-    infix def +++(t2: Term) = append(t1, t2)
-    def map(t2: Term) = self.map(t1, t2)
-    def mapTr(t2: Term, t3: Term) = self.mapTr(t1, t2, t3)
-  }
-  given Conversion[Term, TermProxy] = TermProxy(_)
-  given Conversion[VariableLabel, TermProxy] = v => TermProxy(v())
-
-  object append {
-    val append_ = ConstantFunctionLabel("append", 2)
-    theory.addSymbol(append_)
-
-    val NilCase = theory.addAxiom("append.NilCase", (Nil +++ xs) === xs).get
-    val ConsCase = theory.addAxiom("append.ConsCase", ((x :: xs) +++ ys) === Cons(x, append(xs, ys))).get
-
-    def apply(t1: Term, t2: Term) = append_(t1, t2)
-  }
-
-  object map {
-    val map = ConstantFunctionLabel("map", 2)
-    theory.addSymbol(map)
-    val NilCase = theory.addAxiom("map.NilCase", Nil.map(f) === Nil).get
-    val ConsCase = theory.addAxiom("map.ConsCase", (x :: xs).map(f) === (app(f, x) :: xs.map(f))).get
-    def apply(t1: Term, t2: Term) = map(t1, t2)
-  }
-
-  object mapTr {
-    val mapTr = ConstantFunctionLabel("mapTr", 3)
-    theory.addSymbol(mapTr)
-    val NilCase = theory.addAxiom("mapTr.NilCase", Nil.mapTr(f, xs) === xs).get
-    val ConsCase = theory.addAxiom("mapTr.ConsCase", (x :: xs).mapTr(f, ys) === xs.mapTr(f, ys +++ (app(f, x) :: Nil))).get
-    def apply(t1: Term, t2: Term, t3: Term) = mapTr(t1, t2, t3)
-  }
-
-
-
-  // some more DSL
-
-  val mapRules = Seq(
-    map.NilCase,
-    map.ConsCase,
-    mapTr.NilCase,
-    mapTr.ConsCase,
-    append.NilCase,
-    append.ConsCase
-  )
-
-  object Auto extends ProofTactic {
-
-    def apply(using lib: lisa.prooflib.Library, proof: lib.Proof)
-         (args: proof.Fact | RunningTheory#Justification)(premise: proof.Fact)(bot: Sequent): proof.ProofTacticJudgement = {
-      val tac: proof.ProofTacticJudgement = Substitution.apply2(false, args)(premise)(bot)
-      tac match {
-        case proof.ValidProofTactic(a, b) => proof.ValidProofTactic(a, b)
-        case proof.InvalidProofTactic(m1) =>
-          val tac: proof.ProofTacticJudgement = Substitution.apply2(true, args)(premise)(bot)
-          tac match {
-            case proof.ValidProofTactic(a, b) => proof.ValidProofTactic(a, b)
-            case proof.InvalidProofTactic(m2) =>
-              val tac: proof.ProofTacticJudgement = Tautology.from(args.asInstanceOf, premise)(bot)
-              tac match {
-                case proof.ValidProofTactic(a, b) => proof.ValidProofTactic(a, b)
-                case proof.InvalidProofTactic(m3) => proof.InvalidProofTactic("Decomposition of Auto failure:\n" + m1 + "\n" + m2 + "\n" + m3)
-              }
-          }
-      }
-    }
-
-    def a(using lib: lisa.prooflib.Library, proof: lib.Proof)
-             (args: proof.Fact | RunningTheory#Justification)(bot: Sequent): proof.ProofTacticJudgement = {
-      val tac: proof.ProofTacticJudgement = Tautology.from(args.asInstanceOf)(bot)
-      tac match {
-        case proof.ValidProofTactic(a, b) => proof.ValidProofTactic(a, b)
-        case proof.InvalidProofTactic(m3) => proof.InvalidProofTactic("Decomposition of Auto failure:\n" + m3)
-      }
-    }
-  }
-   */
-}
diff --git a/lisa-examples/src/main/scala/MapProofTest.scala b/lisa-examples/src/main/scala/MapProofTest.scala
deleted file mode 100644
index c66b1c118319a8a7f92e264cc30d1467cd2377b5..0000000000000000000000000000000000000000
--- a/lisa-examples/src/main/scala/MapProofTest.scala
+++ /dev/null
@@ -1,150 +0,0 @@
-import MapProofDef.{_, given}
-import lisa.automation.kernel.OLPropositionalSolver.*
-import lisa.kernel.fol.FOL.*
-import lisa.kernel.proof.RunningTheory
-import lisa.kernel.proof.SCProofChecker.*
-import lisa.kernel.proof.SequentCalculus.*
-import lisa.mathematics.settheory.SetTheory.*
-import lisa.prooflib.BasicStepTactic.*
-import lisa.prooflib.ProofTacticLib.*
-import lisa.prooflib.Substitution.ApplyRules
-import lisa.utils.FOLPrinter.*
-import lisa.utils.KernelHelpers.checkProof
-import lisa.utils.parsing.FOLPrinter
-import lisa.utils.unification.UnificationUtils.*
-
-/**
- * A set of proofs from a functional programming exam about equivalence between
- * `map` and a tail-recursive version of it, `mapTr`.
- *
- * An example of really domain specific proofs using infix extensions.
- */
-object MapProofTest extends lisa.Main {
-  /*
-  val Nil = variable
-  val Cons = function(2)
-  val append = function(2)
-  val x = variable
-  val y = variable
-  val xs = variable
-  val ys = variable
-  val f = variable
-
-  val map_ = function(2)
-  val mapTr_ = function(3)
-
-  // some more DSL
-  extension (t1: Term) {
-    infix def ::(t2: Term) = Cons(t1, t2)
-    infix def ++(t2: Term) = append(t1, t2)
-    def map(t2: Term) = map_(t1, t2)
-    def mapTr(t2: Term, t3: Term) = mapTr_(t1, t2, t3)
-  }
-
-  // available rules
-  val MapNil = Nil.map(f) === Nil
-  val MapCons = forall(x, forall(xs, (x :: xs).map(f) === (app(f, x) :: xs.map(f))))
-  val MapTrNil = forall(xs, Nil.mapTr(f, xs) === xs)
-  val MapTrCons = forall(x, forall(xs, forall(ys, (x :: xs).mapTr(f, ys) === xs.mapTr(f, ys ++ (app(f, x) :: Nil)))))
-  val NilAppend = forall(xs, (Nil ++ xs) === xs)
-  val ConsAppend = forall(x, forall(xs, forall(ys, ((x :: xs) ++ ys) === (x :: (xs ++ ys)))))
-
-  val AccOutNil = Theorem(
-    Nil.mapTr(f, (x :: xs)) === (x :: Nil.mapTr(f, xs))
-  ) {
-    assume(MapTrNil)
-
-    // apply MapTrNil
-    have(Nil.mapTr(f, (x :: xs)) === (x :: xs)) by InstantiateForall
-
-    // apply MapTrNil again
-    thenHave(Nil.mapTr(f, xs) === xs |- Nil.mapTr(f, (x :: xs)) === (x :: Nil.mapTr(f, xs))) by ApplyRules(Nil.mapTr(f, xs) === xs)
-    thenHave(thesis) by LeftForall
-  }
-
-  // induction hypothesis
-  val IH1 = forall(y, forall(ys, xs.mapTr(f, y :: ys) === (y :: xs.mapTr(f, ys))))
-
-  val AccOutCons = Theorem(
-    IH1 |- (x :: xs).mapTr(f, y :: ys) === (y :: (x :: xs).mapTr(f, ys))
-  ) {
-
-    assume(mapRules)
-    assume(IH1)
-
-    // apply MapTrCons
-    have(MapTrCons) by Restate
-    val appYYs = thenHave((x :: xs).mapTr(f, (y :: ys)) === xs.mapTr(f, (y :: ys) ++ (app(f, x) :: Nil))) by InstantiateForall(x, xs, (y :: ys))
-
-    // apply ConsAppend
-    have(ConsAppend) by Restate
-    thenHave((y :: ys) ++ (app(f, x) :: Nil) === (y :: (ys ++ (app(f, x) :: Nil)))) by InstantiateForall(y, ys, (app(f, x) :: Nil))
-
-    val consYYs = have((x :: xs).mapTr(f, (y :: ys)) === xs.mapTr(f, (y :: (ys ++ (app(f, x) :: Nil))))) by ApplyRules(lastStep)(appYYs)
-
-    // apply IH1
-    have(IH1) by Restate
-    thenHave(xs.mapTr(f, (y :: (ys +++ (app(f, x) :: Nil)))) === (y :: xs.mapTr(f, (ys +++ (app(f, x) :: Nil))))) by InstantiateForall(y, (ys +++ (app(f, x) :: Nil)))
-
-    val consYXs = have((x :: xs).mapTr(f, (y :: ys)) === (y :: xs.mapTr(f, (ys ++ (app(f, x) :: Nil))))) by ApplyRules(lastStep)(consYYs)
-
-    // apply mapTr.ConsCase again
-    have(mapTr.ConsCase) by Restate
-    thenHave((x :: xs).mapTr(f, ys) === xs.mapTr(f, (ys +++ (app(f, x) :: Nil)))) by InstantiateForall(x, xs, ys)
-
-    have(thesis) by ApplyRules(lastStep)(consYXs)
-  }
-  show
-
-  val MapEqMapTrNil = Theorem(
-    mapRules |- Nil.map(f) === Nil.mapTr(f, Nil)
-  ) {
-    assume(mapRules)
-
-    // apply MapTrNil
-    val trNil = have(Nil.mapTr(f, Nil) === Nil) by InstantiateForall
-
-    // apply MapNil
-    have(MapNil) by Restate
-    have(thesis) by ApplyRules(trNil)(lastStep)
-  }
-  show
-
-  // the result of induction on the cases above
-  val AccOut = forall(xs, IH1)
-
-  // second induction hypothesis
-  val IH2 = xs.map(f) === xs.mapTr(f, Nil)
-
-  val MapEqMapCons = Theorem(
-    (mapRules :+ IH2 :+ AccOut) |- (x :: xs).map(f) === (x :: xs).mapTr(f, Nil)
-  ) {
-    assume(mapRules)
-    assume(IH2)
-    assume(AccOut)
-
-    // apply map.ConsCase
-    have(map.ConsCase)
-    val mCons = thenHave((x :: xs).map(f) === (app(f, x) :: xs.map(f))) by InstantiateForall(x, xs)
-
-    // apply IH2
-    have(IH2) by Restate
-    val consTr = have((x :: xs).map(f) === (app(f, x) :: xs.mapTr(f, Nil))) by ApplyRules(lastStep)(mCons)
-
-    // apply AccOut
-    have(IH1) by InstantiateForall
-    thenHave(xs.mapTr(f, (app(f, x) :: Nil)) === (app(f, x) :: xs.mapTr(f, Nil))) by InstantiateForall(app(f, x), Nil)
-    val trCons = have((x :: xs).map(f) === xs.mapTr(f, (app(f, x) :: Nil))) by ApplyRules(lastStep)(consTr)
-
-    // apply NilAppend
-    have((Nil ++ (app(f, x) :: Nil)) === (app(f, x) :: Nil)) by InstantiateForall
-    val trApp = have((x :: xs).map(f) === xs.mapTr(f, (Nil ++ (app(f, x) :: Nil)))) by ApplyRules(lastStep)(trCons)
-
-    // apply mapTr.ConsCase
-    have(mapTr.ConsCase)
-    thenHave((x :: xs).mapTr(f, Nil) === xs.mapTr(f, (Nil +++ (app(f, x) :: Nil)))) by InstantiateForall(x, xs, Nil)
-
-    have(thesis) by ApplyRules(lastStep)(trApp)
-  }
-  show*/
-}
diff --git a/lisa-kernel/src/main/scala/lisa/kernel/fol/EquivalenceChecker.scala b/lisa-kernel/src/main/scala/lisa/kernel/fol/EquivalenceChecker.scala
index adfeb547170d2d18e7a8f003c1c1fced7a313631..0965b225fe82e74a83a498df867688bcad941bfe 100644
--- a/lisa-kernel/src/main/scala/lisa/kernel/fol/EquivalenceChecker.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/fol/EquivalenceChecker.scala
@@ -23,6 +23,14 @@ private[fol] trait EquivalenceChecker extends FormulaDefinitions {
     val res = toFormulaAIG(fln)
     res
   }
+
+  def reducedNNFForm(formula: Formula): Formula = {
+    val p = simplify(formula)
+    val nf = computeNormalForm(p)
+    val fln = fromLocallyNameless(nf, Map.empty, 0)
+    val res = toFormulaNNF(fln)
+    res
+  }
   def reduceSet(s: Set[Formula]): Set[Formula] = {
     var res: List[Formula] = Nil
     s.map(reducedForm)
@@ -54,6 +62,12 @@ private[fol] trait EquivalenceChecker extends FormulaDefinitions {
   def isSameSet(s1: Set[Formula], s2: Set[Formula]): Boolean =
     isSubset(s1, s2) && isSubset(s2, s1)
 
+  def isSameSetL(s1: Set[Formula], s2: Set[Formula]): Boolean =
+    isSame(ConnectorFormula(And, s1.toSeq), ConnectorFormula(And, s2.toSeq))
+
+  def isSameSetR(s1: Set[Formula], s2: Set[Formula]): Boolean =
+    isSame(ConnectorFormula(Or, s2.toSeq), ConnectorFormula(Or, s1.toSeq))
+
   def contains(s: Set[Formula], f: Formula): Boolean = {
     s.exists(g => isSame(f, g))
   }
@@ -65,6 +79,7 @@ private[fol] trait EquivalenceChecker extends FormulaDefinitions {
     val size: Int
     var inverse: Option[SimpleFormula] = None
     private[EquivalenceChecker] var normalForm: Option[NormalFormula] = None
+    def getNormalForm = normalForm
   }
   case class SimplePredicate(id: PredicateLabel, args: Seq[Term], polarity: Boolean) extends SimpleFormula {
     override def toString: String = s"SimplePredicate($id, $args, $polarity)"
@@ -143,6 +158,41 @@ private[fol] trait EquivalenceChecker extends FormulaDefinitions {
       r
     }
 
+  /**
+   * Puts back in regular formula syntax, and performs negation normal form to produce shorter version.
+   */
+  def toFormulaNNF(f: NormalFormula, positive: Boolean = true): Formula = {
+    if (positive){
+      if (f.formulaP.isDefined) return f.formulaP.get
+      if (f.inverse.isDefined && f.inverse.get.formulaN.isDefined) return f.inverse.get.formulaN.get
+    }
+    else if (!positive) {
+      if (f.formulaN.isDefined) return f.formulaN.get
+      if (f.inverse.isDefined && f.inverse.get.formulaP.isDefined) return f.inverse.get.formulaP.get
+    }
+    val r = f match{
+      case NormalPredicate(id, args, polarity) =>
+        if (positive==polarity)  PredicateFormula(id, args) else ConnectorFormula(Neg, Seq(PredicateFormula(id, args)))
+      case NormalSchemConnector(id, args, polarity) =>
+        val f = ConnectorFormula(id, args.map(toFormulaNNF(_, true)))
+        if (positive==polarity)  f else ConnectorFormula(Neg, Seq(f))
+      case NormalAnd(args, polarity) =>
+        if (positive==polarity) 
+          ConnectorFormula(And, args.map(c => toFormulaNNF(c, true)))
+        else
+          ConnectorFormula(Or, args.map(c => toFormulaNNF(c, false)))
+      case NormalForall(x, inner, polarity) =>
+        if (positive==polarity) 
+          BinderFormula(Forall, VariableLabel(x), toFormulaNNF(inner, true))
+        else
+          BinderFormula(Exists, VariableLabel(x), toFormulaNNF(inner, false))
+      case NormalLiteral(polarity) => if (polarity) PredicateFormula(top, Seq()) else PredicateFormula(bot, Seq())
+    }
+    if (positive) f.formulaP = Some(r)
+    else  f.formulaN = Some(r)
+    r
+  }
+
   /**
    * Inverse a formula in Polar normal form. Corresponds semantically to taking the negation of the formula.
    */
@@ -322,8 +372,7 @@ private[fol] trait EquivalenceChecker extends FormulaDefinitions {
 
     }
   }
-
-  def reduce(children: Seq[NormalFormula], polarity: Boolean): NormalFormula = {
+  def reduceList(children: Seq[NormalFormula], polarity: Boolean): List[NormalFormula] = {
     val nonSimplified = NormalAnd(children, polarity)
     var remaining: Seq[NormalFormula] = Nil
     def treatChild(i: NormalFormula): Seq[NormalFormula] = {
@@ -366,6 +415,11 @@ private[fol] trait EquivalenceChecker extends FormulaDefinitions {
         accepted = current :: accepted
       }
     }
+    accepted
+  }
+
+  def reduce(children: Seq[NormalFormula], polarity: Boolean): NormalFormula = {
+    val accepted: List[NormalFormula] = reduceList(children, polarity)
     val r = {
       if (accepted.isEmpty) NormalLiteral(polarity)
       else if (accepted.size == 1)
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 4305758460dca63378964c07342cbb43b6ddb99d..4ff7416bdb0ef4ce3fc76d386999add986cbeb0f 100644
--- a/lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaDefinitions.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaDefinitions.scala
@@ -21,7 +21,7 @@ private[fol] trait FormulaDefinitions extends FormulaLabelDefinitions with TermD
    * A formula is a tree whose nodes are either terms or labeled by predicates or logical connectors.
    */
   sealed trait Formula extends TreeWithLabel[FormulaLabel] {
-    private[fol] val uniqueNumber: Long = Formula.getNewId
+    val uniqueNumber: Long = Formula.getNewId
     private[fol] var polarFormula: Option[SimpleFormula] = None
     val arity: Int = label.arity
 
diff --git a/lisa-utils/src/test/scala/lisa/kernel/EquivalenceCheckerTests.scala b/lisa-utils/src/test/scala/lisa/kernel/EquivalenceCheckerTests.scala
index 8afa25d62f7fa0d785f6438aa4dc0d3a10df0c34..d4cf7f0ec3afaa6bbed39647e319b488ff2450cb 100644
--- a/lisa-utils/src/test/scala/lisa/kernel/EquivalenceCheckerTests.scala
+++ b/lisa-utils/src/test/scala/lisa/kernel/EquivalenceCheckerTests.scala
@@ -150,11 +150,11 @@ class EquivalenceCheckerTests extends AnyFunSuite {
 
     // 2. Random formulas (small)
 
-    testWithRepeat(() => formulasGenerator(0.8)(random), 100)
+    testWithRepeat(() => formulasGenerator(0.8)(random), 5)
 
     // 3. Random formulas (larger)
 
-    testWithRepeat(() => formulasGenerator(0.99)(random), 100)
+    testWithRepeat(() => formulasGenerator(0.90)(random), 15)
   }
 
   def testcases(f: Formula => Random => Seq[(Formula, Formula)], equivalent: Boolean): Unit =
@@ -358,8 +358,6 @@ class EquivalenceCheckerTests extends AnyFunSuite {
           Seq(
             and(a, a) -> a,
             or(a, a) -> a
-            // or(or(a, neg(a)), c) -> c,
-            // and(and(a, neg(a)), c) -> and(a, neg(a)),
           ),
       equivalent = true
     )
diff --git a/lisa-utils/src/test/scala/lisa/test/utils/PrinterTest.scala b/lisa-utils/src/test/scala/lisa/test/utils/PrinterTest.scala
index 5b1b65ba63ffd9d36affec591710be4af0c2eedc..521d14435abfca1819b50d052ec94c544e321891 100644
--- a/lisa-utils/src/test/scala/lisa/test/utils/PrinterTest.scala
+++ b/lisa-utils/src/test/scala/lisa/test/utils/PrinterTest.scala
@@ -293,7 +293,7 @@ class PrinterTest extends AnyFunSuite with TestUtils {
     assert(parser.printTerm(Term(plus, Seq(cx, cy))) == "x + y")
     assert(parser.printTerm(Term(plus, Seq(Term(plus, Seq(cx, cy)), cz))) == "x + y + z")
   }
-
+  /*
   test("mix of infix functions and infix predicates") {
     val parser = Parser(SynonymInfoBuilder().addSynonyms(in.id, "∊").addSynonyms(plus.id, "+").build, "∊" :: Nil, ("+", Associativity.Left) :: Nil)
     assert(parser.printFormula(PredicateFormula(in, Seq(Term(plus, Seq(cx, cy)), cz))) == "x + y ∊ z")
@@ -306,5 +306,5 @@ class PrinterTest extends AnyFunSuite with TestUtils {
       ) == "x ∊ y ∧ x ∊ z ∧ x + y ∊ z"
     )
 
-  }
+  }*/
 }
diff --git a/src/main/scala/lisa/automation/Tableau.scala b/src/main/scala/lisa/automation/Tableau.scala
new file mode 100644
index 0000000000000000000000000000000000000000..e5877d7344d7fa63333f79ea3d46d9fd2fddb76d
--- /dev/null
+++ b/src/main/scala/lisa/automation/Tableau.scala
@@ -0,0 +1,403 @@
+package lisa.automation
+import lisa.fol.FOL as F
+import lisa.prooflib.Library
+import lisa.prooflib.ProofTacticLib.*
+import lisa.utils.K
+import lisa.utils.K.{_, given}
+import lisa.utils.parsing.FOLPrinter.prettyFormula
+import lisa.utils.parsing.FOLPrinter.prettySCProof
+import lisa.utils.parsing.FOLPrinter.prettyTerm
+
+import scala.collection.immutable.HashMap
+import scala.collection.immutable.HashSet
+
+/**
+ * Now need to deal with variables unifying with terms containing themselves
+ * optimiye list siye computation
+ * Then, optimize unification check by not checking all pairs all the time
+ * Then, shortcut branches by checking if they are OL-true or OL-false
+ *
+ * Next test: No quantifiers but actual terms with variables
+ */
+
+object Tableau extends ProofTactic with ProofSequentTactic with ProofFactSequentTactic {
+
+  def apply(using lib: Library, proof: lib.Proof)(bot: F.Sequent): proof.ProofTacticJudgement = {
+    solve(bot) match {
+      case Some(value) => proof.ValidProofTactic(bot, value.steps, Seq())
+      case None => proof.InvalidProofTactic("Could not prove the statement.")
+    }
+  }
+
+  /**
+   * Given a targeted conclusion sequent, try to prove it using laws of propositional logic and reflexivity and symmetry of equality.
+   * Uses the given already proven facts as assumptions to reach the desired goal.
+   *
+   * @param proof The ongoing proof object in which the step happens.
+   * @param premise A previously proven step necessary to reach the conclusion.
+   * @param bot   The desired conclusion.
+   */
+  def apply(using lib: Library, proof: lib.Proof)(premise: proof.Fact)(bot: F.Sequent): proof.ProofTacticJudgement =
+    from(using lib, proof)(Seq(premise)*)(bot)
+
+  def from(using lib: Library, proof: lib.Proof)(premises: proof.Fact*)(bot: F.Sequent): proof.ProofTacticJudgement = {
+    val botK = bot.underlying
+    val premsFormulas: Seq[((proof.Fact, Formula), Int)] = premises.map(p => (p, sequentToFormula(proof.getSequent(p).underlying))).zipWithIndex
+    val initProof = premsFormulas.map(s => Restate(() |- s._1._2, -(1 + s._2))).toList
+    val sqToProve = botK ++<< (premsFormulas.map(s => s._1._2).toSet |- ())
+
+    solve(sqToProve) match {
+      case Some(value) =>
+        val subpr = SCSubproof(value)
+        val stepsList = premsFormulas.foldLeft[List[SCProofStep]](List(subpr))((prev: List[SCProofStep], cur) => {
+          val ((prem, form), position) = cur
+          Cut(prev.head.bot -<< form, position, initProof.length + prev.length - 1, form) :: prev
+        })
+        val steps = (initProof ++ stepsList.reverse).toIndexedSeq
+        proof.ValidProofTactic(bot, steps, premises)
+      case None =>
+        proof.InvalidProofTactic("Could not prove the statement.")
+    }
+  }
+
+  inline def solve(sequent: F.Sequent): Option[SCProof] = solve(sequent.underlying)
+
+  def solve(sequent: K.Sequent): Option[SCProof] = {
+    val f = K.ConnectorFormula(K.And, (sequent.left.toSeq ++ sequent.right.map(f => K.ConnectorFormula(K.Neg, List(f)))))
+    val taken = f.schematicTermLabels
+    val nextIdNow = if taken.isEmpty then 0 else taken.maxBy(_.id.no).id.no + 1
+    val (fnamed, nextId, _) = makeVariableNamesUnique(f, nextIdNow, f.freeVariables)
+    val nf = reducedNNFForm(fnamed)
+    val proof = decide(Branch.empty.prepended(nf))
+
+    proof match
+      case None => None
+      case Some((p, _)) => Some(SCProof((Restate(sequent, p.length) :: Weakening(nf |- (), p.length - 1) :: p).reverse.toIndexedSeq, IndexedSeq.empty))
+
+  }
+
+  /**
+   * A branch represent a sequent (whose right hand side is empty) that is being proved.
+   * It is assumed that the sequent is in negation normal form, negations are only applied to atoms.
+   * Formulas are sorted according to their shape :
+   * Conjunctions are in alpha
+   * Disjunctions are in beta
+   * Existential quantifiers are in delta
+   * Universal quantifiers are in gamma
+   * Atoms are in atoms (split into positive and negative)
+   * At each step of the procedure, a formula is deconstructed in accordance with the rules of the tableau calculus.
+   * Then that formula is removed from the branch as it is no longer needed.
+   * Variables coming from universal quantifiers are marked as suitable for unification in unifiable
+   * Instantiations that have been done already are stored in triedInstantiation, to avoid infinite loops.
+   * When a quantifier Q1 is below a universal quantifier Q2, Q2 can be instantiated multiple times.
+   * Then, Q1 may also need to be instantiated multiple versions, requiring fresh variable names.
+   * maxIndex stores an index that is used to generate fresh variable names.
+   */
+  case class Branch(
+      alpha: List[ConnectorFormula], // label = And
+      beta: List[ConnectorFormula], // label = Or
+      delta: List[BinderFormula], // Exists(...))
+      gamma: List[BinderFormula], // Forall(...)
+      atoms: (List[PredicateFormula], List[PredicateFormula]), // split into positive and negatives!
+      unifiable: Map[VariableLabel, BinderFormula], // map between metavariables and the original formula they came from
+      skolemized: Set[VariableLabel], // set of variables that have been skolemized
+      triedInstantiation: Map[VariableLabel, Set[Term]], // map between metavariables and the term they were already instantiated with
+      maxIndex: Int // the maximum index used for skolemization and metavariables
+  ) {
+    def pop(f: Formula): Branch = f match
+      case f @ ConnectorFormula(Or, args) =>
+        if (beta.nonEmpty && beta.head.uniqueNumber == f.uniqueNumber) copy(beta = beta.tail) else throw Exception("First formula of beta is not f")
+      case f @ BinderFormula(Exists, x, inner) =>
+        if (delta.nonEmpty && delta.head.uniqueNumber == f.uniqueNumber) copy(delta = delta.tail) else throw Exception("First formula of delta is not f")
+      case f @ BinderFormula(Forall, x, inner) =>
+        if (gamma.nonEmpty && gamma.head.uniqueNumber == f.uniqueNumber) copy(gamma = gamma.tail) else throw Exception("First formula of gamma is not f")
+      case ConnectorFormula(And, args) =>
+        if (alpha.nonEmpty && alpha.head.uniqueNumber == f.uniqueNumber) copy(alpha = alpha.tail) else throw Exception("First formula of alpha is not f")
+      case f @ PredicateFormula(id, args) =>
+        throw Exception("Should not pop Atoms")
+      case f @ ConnectorFormula(Neg, List(PredicateFormula(id, args))) =>
+        throw Exception("Should not pop Atoms")
+      case _ => ???
+
+    def prepended(f: Formula): Branch = f match
+      case f @ ConnectorFormula(And, args) => this.copy(alpha = f :: alpha)
+      case f @ ConnectorFormula(Or, args) => this.copy(beta = f :: beta)
+      case f @ BinderFormula(Exists, x, inner) => this.copy(delta = f :: delta)
+      case f @ BinderFormula(Forall, x, inner) => this.copy(gamma = f :: gamma)
+      case f @ PredicateFormula(id, args) =>
+        this.copy(atoms = (f :: atoms._1, atoms._2))
+      case ConnectorFormula(Neg, List(f @ PredicateFormula(id, args))) =>
+        this.copy(atoms = (atoms._1, f :: atoms._2))
+      case _ => ???
+
+    def prependedAll(l: Seq[Formula]): Branch = l.foldLeft(this)((a, b) => a.prepended(b))
+
+    def asSequent: Sequent = (beta ++ delta ++ gamma ++ atoms._1 ++ atoms._2.map(a => !a)).toSet |- Set() // inefficient, not used
+
+    import Branch.*
+    override def toString(): String =
+      val pretUnif = unifiable.map((x, f) => x.id + " -> " + prettyFormula(f)).mkString("Unif(", ", ", ")")
+      // val pretTried = triedInstantiation.map((x, t) => x.id + " -> " + prettyTerm(t, true)).mkString("Tried(", ", ", ")")
+      s"Branch(${prettyIte(beta, "beta")}, ${prettyIte(delta, "delta")}, ${prettyIte(gamma, "gamma")}, ${prettyIte(atoms._1, "+")}, ${prettyIte(atoms._2, "-")}, $pretUnif, _, _)"
+
+  }
+  object Branch {
+    def empty = Branch(Nil, Nil, Nil, Nil, (Nil, Nil), Map.empty, Set.empty, Map.empty, 1)
+    def empty(n: Int) = Branch(Nil, Nil, Nil, Nil, (Nil, Nil), Map.empty, Set.empty, Map.empty, n)
+    def prettyIte(l: Iterable[Formula], head: String): String = l match
+      case Nil => "Nil"
+      case _ => l.map(prettyFormula(_, true)).mkString(head + "(", ", ", ")")
+
+  }
+
+  def makeVariableNamesUnique(f: Formula, nextId: Int, seen: Set[VariableLabel]): (Formula, Int, Set[VariableLabel]) = f match
+    case ConnectorFormula(label, args) =>
+      val (nArgs, nnId, nSeen) = args.foldLeft((List(): Seq[Formula], nextId, seen))((prev, next) =>
+        val (l, n, s) = prev
+        val (nf, nn, ns) = makeVariableNamesUnique(next, n, s)
+        (l :+ nf, nn, ns)
+      )
+      (ConnectorFormula(label, nArgs), nnId, nSeen)
+    case pf: PredicateFormula => (pf, nextId, seen)
+    case BinderFormula(label, x, inner) =>
+      if (seen.contains(x))
+        val (nInner, nnId, nSeen) = makeVariableNamesUnique(inner, nextId + 1, seen)
+        val newX = VariableLabel(Identifier(x.id, nextId))
+        (BinderFormula(label, newX, substituteVariablesInFormula(nInner, Map(x -> newX), Seq())), nnId, nSeen)
+      else
+        val (nInner, nnId, nSeen) = makeVariableNamesUnique(inner, nextId, seen + x)
+        (BinderFormula(label, x, nInner), nnId, nSeen)
+
+  type Substitution = Map[VariableLabel, Term]
+  val Substitution = HashMap
+
+  /**
+   * Detect if two terms can be unified, and if so, return a substitution that unifies them.
+   */
+  def unify(t1: Term, t2: Term, current: Substitution, br: Branch): Option[Substitution] = (t1, t2) match
+    case (VariableTerm(x), VariableTerm(y)) if br.unifiable.contains(x) && br.unifiable.contains(y) =>
+      if (x == y) Some(current) else Some(current + (x -> substituteVariablesInTerm(t2, current)))
+    case (VariableTerm(x), t2: Term) if br.unifiable.contains(x) =>
+      if t2.freeVariables.contains(x) then None
+      else if (current.contains(x)) unify(current(x), t2, current, br)
+      else Some(current + (x -> substituteVariablesInTerm(t2, current)))
+    case (t1: Term, VariableTerm(y)) if br.unifiable.contains(y) =>
+      if t1.freeVariables.contains(y) then None
+      else if (current.contains(y)) unify(t1, current(y), current, br)
+      else Some(current + (y -> substituteVariablesInTerm(t1, current)))
+    case (Term(label1, args1), Term(label2, args2)) =>
+      if label1 == label2 && args1.size == args2.size then
+        args1
+          .zip(args2)
+          .foldLeft(Some(current): Option[Substitution])((prev, next) =>
+            prev match
+              case None => None
+              case Some(s) => unify(next._1, next._2, s, br)
+          )
+      else None
+
+  /**
+   * Detect if two atoms can be unified, and if so, return a substitution that unifies them.
+   */
+  def unifyPred(pos: PredicateFormula, neg: PredicateFormula, br: Branch): Option[Substitution] = {
+    (pos, neg) match
+      case (PredicateFormula(id1, args1), PredicateFormula(id2, args2)) if (id1 == id2 && args1.size == args2.size) =>
+        args1
+          .zip(args2)
+          .foldLeft(Some(Substitution.empty): Option[Substitution])((prev, next) =>
+            prev match
+              case None => None
+              case Some(s) => unify(next._1, next._2, s, br)
+          )
+      case _ => None
+
+  }
+
+  /**
+   * Detect if a branch can be closed, and if so, return a list of substitutions that closes it along with the formulas used to close it
+   * If it can't be closed, returns None
+   * The substitution cannot do substitutions that were already done in branch.triedInstantiation.
+   * When multiple substitutions are possible, the one with the smallest size is returned. (Maybe there is a better heuristic, like distance from the root?)
+   */
+  def close(branch: Branch): Option[(Substitution, Set[Formula])] = {
+    val pos = branch.atoms._1.iterator
+    var substitutions: List[(Substitution, Set[Formula])] = Nil
+
+    while (pos.hasNext) {
+      val p = pos.next()
+      if (p.label == bot) return Some((Substitution.empty, Set(bot)))
+      val neg = branch.atoms._2.iterator
+      while (neg.hasNext) {
+        val n = neg.next()
+        unifyPred(p, n, branch) match
+          case None => ()
+          case Some(unif) => substitutions = (unif, Set(p, !n)) :: substitutions
+      }
+    }
+    val cr = substitutions.filterNot(s =>
+      s._1.exists((x, t) =>
+        val v = branch.triedInstantiation.contains(x) && branch.triedInstantiation(x).contains(t)
+        v
+      )
+    )
+    cr.sortBy(_._1.size).headOption
+  }
+
+  /**
+   * Explodes one And formula
+   * The alpha list of the branch must not be empty
+   */
+  def alpha(branch: Branch): Branch = {
+    val f = branch.alpha.head
+    branch.copy(alpha = branch.alpha.tail).prependedAll(f.args)
+  }
+
+  /**
+   * Explodes one Or formula, and alpha-simplifies it
+   * Add the exploded formula to the used list, if one beta formula is found
+   * The beta list of the branch must not be empty
+   */
+  def beta(branch: Branch): List[(Branch, Formula)] = {
+    val f = branch.beta.head
+    val b1 = branch.copy(beta = branch.beta.tail)
+    val resList = f.args.toList.map(disjunct => {
+      ((b1.prepended(disjunct), disjunct))
+    })
+    resList
+  }
+
+  /**
+   * Explodes one Exists formula
+   * Add the unquantified formula to the branch
+   * Since the bound variable is not marked as suitable for instantiation, it behaves as a constant symbol (skolem)
+   */
+  def delta(branch: Branch): (Branch, VariableLabel, Formula) = {
+    val f = branch.delta.head
+    if branch.skolemized.contains(branch.delta.head.bound) then
+      val newX = VariableLabel(Identifier(f.bound.id.name, branch.maxIndex))
+      val newInner = substituteVariablesInFormula(f.inner, Map(f.bound -> newX), Seq())
+      (branch.copy(delta = branch.delta.tail, maxIndex = branch.maxIndex + 1).prepended(newInner), newX, newInner)
+    else (branch.copy(delta = branch.delta.tail, skolemized = branch.skolemized + f.bound).prepended(f.inner), f.bound, f.inner)
+  }
+
+  /**
+   * Explodes one Forall formula
+   * Add the unquantified formula to the branch and mark the bound variable as suitable for unification
+   * This step will most of the time be cancelled when building the proof, unless any arbitrary instantiation is sufficient to get a proof.
+   */
+  def gamma(branch: Branch): (Branch, VariableLabel, Formula) = {
+    val f = branch.gamma.head
+    val (ni, nb) = branch.unifiable.get(f.bound) match
+      case None =>
+        (f.inner, f.bound)
+      case Some(value) =>
+        val newBound = VariableLabel(Identifier(f.bound.id.name, branch.maxIndex))
+        val newInner = substituteVariablesInFormula(f.inner, Map(f.bound -> newBound), Seq())
+        (newInner, newBound)
+    val b1 = branch.copy(gamma = branch.gamma.tail, unifiable = branch.unifiable + (nb -> f), maxIndex = branch.maxIndex + 1)
+    (b1.prepended(ni), nb, ni)
+  }
+
+  /**
+   * When a closing unification has been found, apply it to the branch
+   * This does not backtracking: The metavariable remains available if it needs further instantiation.
+   */
+  def applyInst(branch: Branch, x: VariableLabel, t: Term): (Branch, Formula) = {
+    val f = branch.unifiable(x)
+    val newTried = branch.triedInstantiation.get(x) match
+      case None => branch.triedInstantiation + (x -> Set(t))
+      case Some(s) => branch.triedInstantiation + (x -> (s + t))
+
+    val inst = instantiate(f.inner, f.bound, t)
+    val r = branch.prepended(inst).copy(triedInstantiation = newTried)
+    (r, inst)
+  }
+
+  /**
+   * Decide if a branch can be closed, and if not, explode it.
+   * Main routine of the decision procedure. If it succeeds, return a proof of the branch.
+   * Note that the proof actually proves a subset of a branch when possible, to cut short on unneeded steps and formulas.
+   * The return integer is the size of the proof: Used to avoid computing the size every time in linear time.
+   */
+  def decide(branch: Branch): Option[(List[SCProofStep], Int)] = {
+    val closeSubst = close(branch)
+    if (closeSubst.nonEmpty && closeSubst.get._1.isEmpty) // If branch can be closed without Instantiation (Hyp)
+      Some((List(RestateTrue(Sequent(closeSubst.get._2, Set()))), 0))
+    else if (branch.alpha.nonEmpty) // If branch contains an Alpha formula (LeftAnd)
+      val rec = alpha(branch)
+      decide(rec).map((proof, step) =>
+        if branch.alpha.head.args.exists(proof.head.bot.left.contains) then
+          val sequent = proof.head.bot.copy(left = (proof.head.bot.left -- branch.alpha.head.args) + branch.alpha.head)
+          (Weakening(sequent, proof.size - 1) :: proof, step + 1)
+        else (proof, step)
+      )
+    else if (branch.delta.nonEmpty) // If branch contains a Delta formula (LeftExists)
+      val rec = delta(branch)
+      val upperProof = decide(rec._1)
+      upperProof.map((proof, step) =>
+        if proof.head.bot.left.contains(rec._3) then
+          val sequent = (proof.head.bot -<< rec._3) +<< branch.delta.head
+          (LeftExists(sequent, step, rec._3, rec._2) :: proof, step + 1)
+        else (proof, step)
+      )
+    else if (branch.beta.nonEmpty) // If branch contains a Beta formula (LeftOr)
+      val list = beta(branch)
+      val (proof, treversed, needed) = list.foldLeft((Some(Nil): Option[List[SCProofStep]], Nil: List[Int], true: Boolean))((prev, next) =>
+        prev match
+          case (None, _, _) => prev // proof failed
+          case (_, _, false) =>
+            prev // proof succeded early
+          case (Some(prevProof), t, true) =>
+            val res = decide(next._1)
+            res match
+              case None => (None, t, true)
+              case Some((nextProof, step)) =>
+                if nextProof.head.bot.left.contains(next._2) then // If the disjunct was used, encapsulate the subbranch in a Subproof
+                  val subproofDisj =
+                    if nextProof.size == 1 then nextProof.head
+                    else SCSubproof(SCProof(nextProof.toIndexedSeq.reverse, IndexedSeq.empty), IndexedSeq.empty)
+                  (Some(subproofDisj :: prevProof), prevProof.size :: t, true)
+                else
+                  // If the disjunct was not used, then the subbranch is a proof of the whole statement and the split is not necessary.
+                  (res.map(_._1), List(nextProof.size - 1), false)
+      )
+      proof.map(proo =>
+        if needed == true then
+          val sequent = ((proo.flatMap(_.bot.left).toSet -- list.map(_._2)) |- ()) +<< branch.beta.head
+          (LeftOr(sequent, treversed.reverse, branch.beta.head.args) :: proo, treversed.size)
+        else (proo, proo.size - 1)
+      )
+    else if (branch.gamma.nonEmpty) // If branch contains a Gamma formula (LeftForall)
+      val rec = gamma(branch)
+      val upperProof = decide(rec._1)
+      // LeftForall(bot: Sequent, t1: Int, phi: Formula, x: VariableLabel, t: Term)
+      upperProof.map((proof, step) =>
+        if proof.head.bot.left.contains(rec._3) then
+          val sequent = (proof.head.bot -<< rec._3) +<< branch.gamma.head
+          (LeftForall(sequent, step, branch.gamma.head.inner, branch.gamma.head.bound, rec._2()) :: proof, step + 1)
+        else (proof, step)
+      )
+    else if (closeSubst.nonEmpty && closeSubst.get._1.nonEmpty) // If branch can be closed with Instantiation (LeftForall)
+      val (x, t) = closeSubst.get._1.head
+      val (recBranch, instantiated) = applyInst(branch, x, t)
+      val upperProof = decide(recBranch)
+      upperProof.map((proof, step) =>
+        if proof.head.bot.left.contains(instantiated) then
+          val sequent = (proof.head.bot -<< instantiated) +<< branch.unifiable(x)
+          (LeftForall(sequent, step, branch.unifiable(x).inner, branch.unifiable(x).bound, t) :: proof, step + 1)
+        else (proof, step)
+      )
+    else None
+    // End of decide
+  }
+
+  def containsAlpha(set: Set[Formula], f: Formula) = f match {
+    case ConnectorFormula(And, args) => args.exists(set.contains)
+    case _ => set.contains(f)
+  }
+
+  def instantiate(f: Formula, x: VariableLabel, t: Term): Formula = f match
+    case ConnectorFormula(label, args) => ConnectorFormula(label, args.map(instantiate(_, x, t)))
+    case PredicateFormula(id, args) => PredicateFormula(id, args.map(substituteVariablesInTerm(_, Substitution(x -> t))))
+    case BinderFormula(label, y, inner) => if (x == y) f else BinderFormula(label, y, instantiate(inner, x, t))
+}
diff --git a/src/main/scala/lisa/mathematics/fol/Quantifiers.scala b/src/main/scala/lisa/mathematics/fol/Quantifiers.scala
index e00288545be71d3a3d0c87fe9a6cd702d57a9249..0d0a64c1339b6b8d7b3da80fdfbe68bff22d2018 100644
--- a/src/main/scala/lisa/mathematics/fol/Quantifiers.scala
+++ b/src/main/scala/lisa/mathematics/fol/Quantifiers.scala
@@ -1,6 +1,7 @@
 package lisa.mathematics
 package fol
 
+import lisa.automation.Tableau
 import lisa.automation.kernel.OLPropositionalSolver.Tautology
 import lisa.automation.kernel.SimplePropositionalSolver.*
 import lisa.prooflib.Substitution
@@ -27,15 +28,7 @@ object Quantifiers extends lisa.Main {
   val closedFormulaUniversal = Theorem(
     () |- ∀(x, p) <=> p
   ) {
-    val base = have(p |- p) by Hypothesis
-
-    have(p |- ∀(x, p)) by RightForall(base)
-    val lhs = thenHave(() |- p ==> ∀(x, p)) by Restate
-
-    have(∀(x, p) |- p) by LeftForall(base)
-    val rhs = thenHave(() |- ∀(x, p) ==> p) by Restate
-    have(thesis) by RightIff(lhs, rhs)
-
+    have(thesis) by Tableau
   }
 
   /**
@@ -45,15 +38,7 @@ object Quantifiers extends lisa.Main {
   val closedFormulaExistential = Theorem(
     () |- ∃(x, p) <=> p
   ) {
-    val base = have(p |- p) by Hypothesis
-
-    have(p |- ∃(x, p)) by RightExists(base)
-    val lhs = thenHave(() |- p ==> ∃(x, p)) by Restate
-
-    have(∃(x, p) |- p) by LeftExists(base)
-    val rhs = thenHave(() |- ∃(x, p) ==> p) by Restate
-
-    have(thesis) by RightIff(lhs, rhs)
+    have(thesis) by Tableau
   }
 
   /**
@@ -88,31 +73,7 @@ object Quantifiers extends lisa.Main {
   val universalConjunctionCommutation = Theorem(
     () |- forall(x, P(x) /\ Q(x)) <=> forall(x, P(x)) /\ forall(x, Q(x))
   ) {
-    // forward direction
-    val fwd = have(forall(x, P(x) /\ Q(x)) ==> forall(x, P(x)) /\ forall(x, Q(x))) subproof {
-      have(P(x) /\ Q(x) |- P(x)) by Restate
-      thenHave(forall(x, P(x) /\ Q(x)) |- P(x)) by LeftForall
-      val px = thenHave(forall(x, P(x) /\ Q(x)) |- forall(x, P(x))) by RightForall
-
-      have(P(x) /\ Q(x) |- Q(x)) by Restate
-      thenHave(forall(x, P(x) /\ Q(x)) |- Q(x)) by LeftForall
-      val qx = thenHave(forall(x, P(x) /\ Q(x)) |- forall(x, Q(x))) by RightForall
-
-      have(forall(x, P(x) /\ Q(x)) |- forall(x, P(x)) /\ forall(x, Q(x))) by RightAnd(px, qx)
-      thenHave(thesis) by Restate
-    }
-
-    // backward direction
-    val bwd = have(forall(x, P(x)) /\ forall(x, Q(x)) ==> forall(x, P(x) /\ Q(x))) subproof {
-      have((P(x), Q(x)) |- P(x) /\ Q(x)) by Restate
-      thenHave((forall(x, P(x)), Q(x)) |- P(x) /\ Q(x)) by LeftForall
-      thenHave((forall(x, P(x)), forall(x, Q(x))) |- P(x) /\ Q(x)) by LeftForall
-      thenHave((forall(x, P(x)), forall(x, Q(x))) |- forall(x, P(x) /\ Q(x))) by RightForall
-
-      thenHave(thesis) by Restate
-    }
-
-    have(thesis) by RightIff(fwd, bwd)
+    have(thesis) by Tableau
   }
 
   /**
@@ -121,17 +82,7 @@ object Quantifiers extends lisa.Main {
   val existentialConjunctionDistribution = Theorem(
     exists(x, P(x) /\ Q(x)) |- exists(x, P(x)) /\ exists(x, Q(x))
   ) {
-    have(P(x) |- P(x)) by Hypothesis
-    thenHave(P(x) /\ Q(x) |- P(x)) by Weakening
-    thenHave(P(x) /\ Q(x) |- exists(x, P(x))) by RightExists
-    val left = thenHave(exists(x, P(x) /\ Q(x)) |- exists(x, P(x))) by LeftExists
-
-    have(Q(x) |- Q(x)) by Hypothesis
-    thenHave(P(x) /\ Q(x) |- Q(x)) by Weakening
-    thenHave(P(x) /\ Q(x) |- exists(x, Q(x))) by RightExists
-    val right = thenHave(exists(x, P(x) /\ Q(x)) |- exists(x, Q(x))) by LeftExists
-
-    have(thesis) by RightAnd(left, right)
+    have(thesis) by Tableau
   }
 
   /**
@@ -140,32 +91,7 @@ object Quantifiers extends lisa.Main {
   val existentialConjunctionWithClosedFormula = Theorem(
     exists(x, P(x) /\ p) <=> (exists(x, P(x)) /\ p)
   ) {
-    val forward = have(exists(x, P(x) /\ p) ==> (exists(x, P(x)) /\ p)) subproof {
-      have(exists(x, P(x) /\ p) |- exists(x, P(x)) /\ exists(x, p)) by Restate.from(
-        existentialConjunctionDistribution of (
-          Q -> lambda(x, p)
-        )
-      )
-      val substitution = thenHave(
-        (exists(x, P(x) /\ p), (exists(x, P(x)) /\ exists(x, p)) <=> (exists(x, P(x)) /\ p)) |- exists(x, P(x)) /\ p
-      ) by RightSubstIff(List((exists(x, P(x)) /\ exists(x, p), exists(x, P(x)) /\ p)), lambda(p, p))
-
-      have(exists(x, p) <=> p) by Restate.from(closedFormulaExistential)
-      thenHave((exists(x, P(x)) /\ exists(x, p)) <=> (exists(x, P(x)) /\ p)) by Tautology
-
-      have(exists(x, P(x) /\ p) |- exists(x, P(x)) /\ p) by Cut(lastStep, substitution)
-      thenHave(thesis) by Restate
-    }
-
-    val backward = have((exists(x, P(x)) /\ p) ==> exists(x, P(x) /\ p)) subproof {
-      have(P(x) /\ p |- P(x) /\ p) by Hypothesis
-      thenHave((P(x), p) |- P(x) /\ p) by Restate
-      thenHave((P(x), p) |- exists(x, P(x) /\ p)) by RightExists
-      thenHave((exists(x, P(x)), p) |- exists(x, P(x) /\ p)) by LeftExists
-      thenHave(thesis) by Restate
-    }
-
-    have(thesis) by RightIff(forward, backward)
+    have(thesis) by Tableau
   }
 
   /**
@@ -200,31 +126,7 @@ object Quantifiers extends lisa.Main {
   val existentialDisjunctionCommutation = Theorem(
     () |- exists(x, P(x) \/ Q(x)) <=> exists(x, P(x)) \/ exists(x, Q(x))
   ) {
-    // forward direction
-    val fwd = have(exists(x, P(x) \/ Q(x)) ==> exists(x, P(x)) \/ exists(x, Q(x))) subproof {
-      have(P(x) \/ Q(x) |- (P(x), Q(x))) by Restate
-      thenHave(P(x) \/ Q(x) |- (exists(x, P(x)), Q(x))) by RightExists
-      thenHave(P(x) \/ Q(x) |- (exists(x, P(x)), exists(x, Q(x)))) by RightExists
-      thenHave(exists(x, P(x) \/ Q(x)) |- (exists(x, P(x)), exists(x, Q(x)))) by LeftExists
-
-      thenHave(thesis) by Restate
-    }
-
-    // backward direction
-    val bwd = have(exists(x, P(x)) \/ exists(x, Q(x)) ==> exists(x, P(x) \/ Q(x))) subproof {
-      have(P(x) |- P(x) \/ Q(x)) by Restate
-      thenHave(P(x) |- exists(x, P(x) \/ Q(x))) by RightExists
-      val px = thenHave(exists(x, P(x)) |- exists(x, P(x) \/ Q(x))) by LeftExists
-
-      have(Q(x) |- P(x) \/ Q(x)) by Restate
-      thenHave(Q(x) |- exists(x, P(x) \/ Q(x))) by RightExists
-      val qx = thenHave(exists(x, Q(x)) |- exists(x, P(x) \/ Q(x))) by LeftExists
-
-      have(exists(x, P(x)) \/ exists(x, Q(x)) |- exists(x, P(x) \/ Q(x))) by LeftOr(px, qx)
-      thenHave(thesis) by Restate
-    }
-
-    have(thesis) by RightIff(fwd, bwd)
+    have(thesis) by Tableau
   }
 
   /**
@@ -233,24 +135,7 @@ object Quantifiers extends lisa.Main {
   val universalEquivalenceDistribution = Theorem(
     forall(z, P(z) <=> Q(z)) |- (forall(z, P(z)) <=> forall(z, Q(z)))
   ) {
-    have(forall(z, P(z) <=> Q(z)) |- forall(z, P(z) <=> Q(z))) by Hypothesis
-    val quant = thenHave(forall(z, P(z) <=> Q(z)) |- P(z) <=> Q(z)) by InstantiateForall(z)
-
-    val lhs = have((forall(z, P(z) <=> Q(z)), forall(z, P(z))) |- forall(z, Q(z))) subproof {
-      have(forall(z, P(z)) |- forall(z, P(z))) by Hypothesis
-      thenHave(forall(z, P(z)) |- P(z)) by InstantiateForall(z)
-      have((forall(z, P(z) <=> Q(z)), forall(z, P(z))) |- Q(z)) by Tautology.from(lastStep, quant)
-      thenHave(thesis) by RightForall
-    }
-
-    val rhs = have((forall(z, P(z) <=> Q(z)), forall(z, Q(z))) |- forall(z, P(z))) subproof {
-      have(forall(z, Q(z)) |- forall(z, Q(z))) by Hypothesis
-      thenHave(forall(z, Q(z)) |- Q(z)) by InstantiateForall(z)
-      have((forall(z, P(z) <=> Q(z)), forall(z, Q(z))) |- P(z)) by Tautology.from(lastStep, quant)
-      thenHave(thesis) by RightForall
-    }
-
-    have(thesis) by Tautology.from(lhs, rhs)
+    have(thesis) by Tableau
   }
 
   /**
@@ -260,24 +145,7 @@ object Quantifiers extends lisa.Main {
   val existentialEquivalenceDistribution = Theorem(
     forall(z, P(z) <=> Q(z)) |- (exists(z, P(z)) <=> exists(z, Q(z)))
   ) {
-    have(forall(z, P(z) <=> Q(z)) |- forall(z, P(z) <=> Q(z))) by Hypothesis
-    val quant = thenHave(forall(z, P(z) <=> Q(z)) |- P(z) <=> Q(z)) by InstantiateForall(z)
-
-    val lhs = have((forall(z, P(z) <=> Q(z)), exists(z, P(z))) |- exists(z, Q(z))) subproof {
-      have(P(z) |- P(z)) by Hypothesis
-      have((forall(z, P(z) <=> Q(z)), P(z)) |- Q(z)) by Tautology.from(lastStep, quant)
-      thenHave((forall(z, P(z) <=> Q(z)), P(z)) |- exists(z, Q(z))) by RightExists
-      thenHave(thesis) by LeftExists
-    }
-
-    val rhs = have((forall(z, P(z) <=> Q(z)), exists(z, Q(z))) |- exists(z, P(z))) subproof {
-      have(Q(z) |- Q(z)) by Hypothesis
-      have((forall(z, P(z) <=> Q(z)), Q(z)) |- P(z)) by Tautology.from(lastStep, quant)
-      thenHave((forall(z, P(z) <=> Q(z)), Q(z)) |- exists(z, P(z))) by RightExists
-      thenHave(thesis) by LeftExists
-    }
-
-    have(thesis) by Tautology.from(lhs, rhs)
+    have(thesis) by Tableau
 
   }
 
@@ -287,13 +155,7 @@ object Quantifiers extends lisa.Main {
   val universalImplicationDistribution = Theorem(
     forall(z, P(z) ==> Q(z)) |- (forall(z, P(z)) ==> forall(z, Q(z)))
   ) {
-    have(forall(z, P(z) ==> Q(z)) |- forall(z, P(z) ==> Q(z))) by Hypothesis
-    val quant = thenHave(forall(z, P(z) ==> Q(z)) |- P(z) ==> Q(z)) by InstantiateForall(z)
-
-    have(forall(z, P(z)) |- forall(z, P(z))) by Hypothesis
-    thenHave(forall(z, P(z)) |- P(z)) by InstantiateForall(z)
-    have((forall(z, P(z) ==> Q(z)), forall(z, P(z))) |- Q(z)) by Tautology.from(lastStep, quant)
-    thenHave((forall(z, P(z) ==> Q(z)), forall(z, P(z))) |- forall(z, Q(z))) by RightForall
+    have(thesis) by Tableau
   }
 
   /**
@@ -303,15 +165,7 @@ object Quantifiers extends lisa.Main {
   val existentialImplicationDistribution = Theorem(
     forall(z, P(z) ==> Q(z)) |- (exists(z, P(z)) ==> exists(z, Q(z)))
   ) {
-    have(forall(z, P(z) ==> Q(z)) |- forall(z, P(z) ==> Q(z))) by Hypothesis
-    val quant = thenHave(forall(z, P(z) ==> Q(z)) |- P(z) ==> Q(z)) by InstantiateForall(z)
-
-    val impl = have((forall(z, P(z) ==> Q(z)), exists(z, P(z))) |- exists(z, Q(z))) subproof {
-      have(P(z) |- P(z)) by Hypothesis
-      have((forall(z, P(z) ==> Q(z)), P(z)) |- Q(z)) by Tautology.from(lastStep, quant)
-      thenHave((forall(z, P(z) ==> Q(z)), P(z)) |- exists(z, Q(z))) by RightExists
-      thenHave(thesis) by LeftExists
-    }
+    have(thesis) by Tableau
   }
 
   /**