diff --git a/lisa-utils/src/main/scala/lisa/utils/TheoriesHelpers.scala b/lisa-utils/src/main/scala/lisa/utils/TheoriesHelpers.scala
index 504c9077321f920874c26c4df5d990dfd255ee54..9f6cfbc4858269d67a58d097cfcfeb3dbaf22bf3 100644
--- a/lisa-utils/src/main/scala/lisa/utils/TheoriesHelpers.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/TheoriesHelpers.scala
@@ -27,7 +27,7 @@ trait TheoriesHelpers extends KernelHelpers {
      * of the theorem to have more explicit writing and for sanity check.
      */
     def theorem(name: String, statement: String, proof: SCProof, justifications: Seq[theory.Justification]): RunningTheoryJudgement[theory.Theorem] = {
-      val expected = proof.conclusion // parse(statement)
+      val expected = Parser.parseSequent(statement)
       if (expected == proof.conclusion) theory.makeTheorem(name, expected, proof, justifications)
       else if (isSameSequent(expected, proof.conclusion)) theory.makeTheorem(name, expected, proof.appended(Rewrite(expected, proof.length - 1)), justifications)
       else InvalidJustification("The proof does not prove the claimed statement", None)
diff --git a/src/main/scala/lisa/proven/mathematics/Mapping.scala b/src/main/scala/lisa/proven/mathematics/Mapping.scala
index 337152133287640eeed2e7476d0a4683f6e24208..f318e41090dcd64a142a9cc59d0343b740ea7494 100644
--- a/src/main/scala/lisa/proven/mathematics/Mapping.scala
+++ b/src/main/scala/lisa/proven/mathematics/Mapping.scala
@@ -12,7 +12,7 @@ import SetTheory.*
 object Mapping extends lisa.Main {
 
   THEOREM("functionalMapping") of
-    "∀a. (a ∈ ?A) ⇒ ∃!x. ?phi(x, a) ⊢ ∃!X. ∀x. (x ∈ X) ↔ ∃a. (a ∈ ?A) ∧ ?phi(x, a)" PROOF {
+    "∀ 'a. elem('a, 'A) ⇒ (∃! 'x. 'phi('x, 'a)) ⊢ ∃! 'X. ∀ 'x. elem('x, 'X) ↔ (∃ 'a. elem('a, 'A) ∧ 'phi('x, 'a))" PROOF {
       val a = VariableLabel("a")
       val x = VariableLabel("x")
       val y = VariableLabel("y")
@@ -235,7 +235,8 @@ object Mapping extends lisa.Main {
   show
 
   THEOREM("lemmaLayeredTwoArgumentsMap") of
-    "∀b. (b ∈ ?B) ⇒ ∀a. (a ∈ ?A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∃!X. ∀x. (x ∈ X) ↔ ∃b. (b ∈ ?B) ∧ ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ ?A) ∧ ?psi(x1, a, b)" PROOF {
+    "∀ 'b. elem('b, 'B) ⇒ (∀ 'a. elem('a, 'A) ⇒ (∃! 'x. 'psi('x, 'a, 'b))) ⊢ " +
+    "∃! 'X. ∀ 'x. elem('x, 'X) ↔ (∃ 'b. elem('b, 'B) ∧ (∀ 'x1. elem('x1, 'x) ↔ (∃ 'a. elem('a, 'A) ∧ 'psi('x1, 'a, 'b))))" PROOF {
       val a = VariableLabel("a")
       val b = VariableLabel("b")
       val x = VariableLabel("x")
@@ -299,7 +300,7 @@ object Mapping extends lisa.Main {
   show
 
   THEOREM("applyFunctionToUniqueObject") of
-    "∃!x. ?phi(x) ⊢ ∃!z. ∃x. (z = ?F(x)) ∧ ?phi(x)" PROOF {
+    "∃! 'x. 'phi('x) ⊢ ∃! 'z. ∃ 'x. ('z = 'F('x)) ∧ 'phi('x)" PROOF {
       val x = VariableLabel("x")
       val x1 = VariableLabel("x1")
       val z = VariableLabel("z")
@@ -348,7 +349,8 @@ object Mapping extends lisa.Main {
   show
 
   THEOREM("mapTwoArguments") of
-    "∀b. (b ∈ ?B) ⇒ ∀a. (a ∈ ?A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∃!z. ∃x. (z = U(x)) ∧ ∀x_0. (x_0 ∈ x) ↔ ∃b. (b ∈ ?B) ∧ ∀x1. (x1 ∈ x_0) ↔ ∃a. (a ∈ ?A) ∧ ?psi(x1, a, b)" PROOF {
+    "∀ 'b. elem('b, 'B) ⇒ (∀ 'a. elem('a, 'A) ⇒ (∃! 'x. 'psi('x, 'a, 'b))) ⊢ " +
+    "∃! 'z. ∃ 'x. 'z = union('x) ∧ (∀ 'x_0. elem('x_0, 'x) ↔ (∃ 'b. elem('b, 'B) ∧ (∀ 'x1. elem('x1, 'x_0) ↔ (∃ 'a. elem('a, 'A) ∧ 'psi('x1, 'a, 'b)))))" PROOF {
       val a = VariableLabel("a")
       val b = VariableLabel("b")
       val x = VariableLabel("x")
diff --git a/src/main/scala/lisa/proven/mathematics/SetTheory.scala b/src/main/scala/lisa/proven/mathematics/SetTheory.scala
index 611c82a5ff955d87ce2b3d51a91ec96861be7c61..c02bd0c0f4fe96e3c9987d0f4d9de496655d316d 100644
--- a/src/main/scala/lisa/proven/mathematics/SetTheory.scala
+++ b/src/main/scala/lisa/proven/mathematics/SetTheory.scala
@@ -8,7 +8,7 @@ import lisa.automation.kernel.ProofTactics.*
  */
 object SetTheory extends lisa.Main {
 
-  THEOREM("russelParadox") of "∀x. (x ∈ ?y) ↔ ¬(x ∈ x) ⊢" PROOF {
+  THEOREM("russelParadox") of "∀'x. elem('x, 'y) ↔ ¬elem('x, 'x) ⊢" PROOF {
     val y = VariableLabel("y")
     val x = VariableLabel("x")
     val s0 = RewriteTrue(in(y, y) <=> !in(y, y) |- ())
@@ -18,7 +18,7 @@ object SetTheory extends lisa.Main {
   thm"russelParadox".show
 
   THEOREM("unorderedPair_symmetry") of
-    "⊢ ∀y, x. {x, y} = {y, x}" PROOF {
+    "⊢ ∀'y. ∀'x. unordered_pair('x, 'y) = unordered_pair('y, 'x)" PROOF {
       val x = VariableLabel("x")
       val y = VariableLabel("y")
       val z = VariableLabel("z")
@@ -72,7 +72,7 @@ object SetTheory extends lisa.Main {
 
   // This proof is old and very unoptimised
   THEOREM("unorderedPair_deconstruction") of
-    "⊢ ∀x, y, x', y'. ({x, y} = {x', y'}) ⇒ (y' = y) ∧ (x' = x) ∨ (x = y') ∧ (y = x')" PROOF {
+    "⊢ ∀'x. ∀'y. ∀ 'x1. ∀ 'y1. unordered_pair('x, 'y) = unordered_pair('x1, 'y1) ⇒ 'y1 = 'y ∧ 'x1 = 'x ∨ 'x = 'y1 ∧ 'y = 'x1" PROOF {
       val x = VariableLabel("x")
       val y = VariableLabel("y")
       val x1 = VariableLabel("x'")
@@ -327,7 +327,7 @@ object SetTheory extends lisa.Main {
     } using ax"pairAxiom"
   thm"unorderedPair_deconstruction".show
 
-  THEOREM("noUniversalSet") of "∀x. x ∈ ?z ⊢" PROOF {
+  THEOREM("noUniversalSet") of "∀'x. elem('x, 'z) ⊢ " PROOF {
     val x = VariableLabel("x")
     val y = VariableLabel("y")
     val z = VariableLabel("z")
diff --git a/src/main/scala/lisa/proven/peano_example/Peano.scala b/src/main/scala/lisa/proven/peano_example/Peano.scala
index 90479702b07b208293d19d6e0357e495a03b556e..47642c624698b6782cfd529af4b1d6a5c9b78132 100644
--- a/src/main/scala/lisa/proven/peano_example/Peano.scala
+++ b/src/main/scala/lisa/proven/peano_example/Peano.scala
@@ -66,7 +66,7 @@ object Peano {
   val (y1, z1) =
     (VariableLabel("y1"), VariableLabel("z1"))
 
-  THEOREM("x + 0 = 0 + x") of "?x. plus(x, zero) === plus(zero, x)" PROOF {
+  THEOREM("x + 0 = 0 + x") of "∀'x. +('x, 0) = +(0, 'x)" PROOF {
     val refl0: SCProofStep = RightRefl(() |- s(x) === s(x), s(x) === s(x))
     val subst1 = RightSubstEq((x === plus(zero, x)) |- s(x) === s(plus(zero, x)), 0, (x, plus(zero, x)) :: Nil, LambdaTermFormula(Seq(y), s(x) === s(y)))
     val implies2 = RightImplies(() |- (x === plus(zero, x)) ==> (s(x) === s(plus(zero, x))), 1, x === plus(zero, x), s(x) === s(plus(zero, x)))
@@ -147,7 +147,7 @@ object Peano {
   } using (ax"ax4plusSuccessor", ax"ax3neutral", ax"ax7induction")
   show
 
-  THEOREM("switch successor") of "?y. ?x. plus(x, s(y)) === plus(s(x), y)" PROOF {
+  THEOREM("switch successor") of "∀'x. ∀'y. +('x, S('y)) = +(S('x), 'y)" PROOF {
     //////////////////////////////////// Base: x + S0 = Sx + 0 ///////////////////////////////////////////////
     val base0 = {
       // x + 0 = x
@@ -256,7 +256,7 @@ object Peano {
   } using (ax"ax3neutral", ax"ax4plusSuccessor", ax"ax7induction")
   show
 
-  THEOREM("additivity of addition") of "" PROOF {
+  THEOREM("additivity of addition") of "∀'x. ∀'y. +('x, 'y) = +('y, 'x)" PROOF {
     val base0 = SCSubproof(instantiateForallImport(thm"x + 0 = 0 + x", x), Seq(-3))
     val inductionStep1 = {
       val start0 = RightRefl(() |- plus(x, s(y)) === plus(x, s(y)), plus(x, s(y)) === plus(x, s(y)))