diff --git a/lisa-kernel/src/main/scala/lisa/kernel/fol/CommonDefinitions.scala b/lisa-kernel/src/main/scala/lisa/kernel/fol/CommonDefinitions.scala
index 901989ed75a87d06d4d07ac7efcf9a291238359e..1faa2a2089790ded35da0cb57ae4d7a02c5e4456 100644
--- a/lisa-kernel/src/main/scala/lisa/kernel/fol/CommonDefinitions.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/fol/CommonDefinitions.scala
@@ -6,13 +6,6 @@ package lisa.kernel.fol
 private[fol] trait CommonDefinitions {
   val MaxArity: Int = 1000000
 
-  /**
-   * An object with arity information for tree-like structures.
-   */
-  protected trait Arity {
-    val arity: Int
-  }
-
   /**
    * An labelled node for tree-like structures.
    */
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 27f1bcbb57de39a8619b1320f1f3df4c13b33387..d3252743d03d02a7a784f8a287e4d24c0941da14 100644
--- a/lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaLabelDefinitions.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaLabelDefinitions.scala
@@ -34,7 +34,7 @@ private[fol] trait FormulaLabelDefinitions extends CommonDefinitions {
    * The label for a predicate, namely a function taking a fixed number of terms and returning a formula.
    * In logical terms it is a predicate symbol.
    */
-  sealed abstract class PredicateLabel extends FormulaLabel with Arity {
+  sealed abstract class PredicateLabel extends FormulaLabel {
     require(arity < MaxArity && arity >= 0)
   }
 
@@ -68,7 +68,7 @@ private[fol] trait FormulaLabelDefinitions extends CommonDefinitions {
   /**
    * The label for a connector, namely a function taking a fixed number of formulas and returning another formula.
    */
-  sealed abstract class ConnectorLabel(val id: String, val arity: Int) extends FormulaLabel with Arity {
+  sealed abstract class ConnectorLabel(val id: String, val arity: Int) extends FormulaLabel {
     require(arity < MaxArity && arity >= -1)
   }
 
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 163e8d360cccb891c54f86fce4bb3a9779b68126..3c2ca18d6023d055ff82e040edd23b27c3ad4bee 100644
--- a/lisa-kernel/src/main/scala/lisa/kernel/fol/TermLabelDefinitions.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/fol/TermLabelDefinitions.scala
@@ -35,7 +35,7 @@ private[fol] trait TermLabelDefinitions extends CommonDefinitions {
    * Standard function symbols denote a particular function. Schematic function symbols
    * can be instantiated with any term. This is particularly useful to express axiom schemas.
    */
-  sealed abstract class FunctionLabel extends TermLabel with Arity {
+  sealed abstract class FunctionLabel extends TermLabel {
     require(arity >= 0 && arity < MaxArity)
   }
 
diff --git a/lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala b/lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala
index 1452de69e93e7c051afa06c4e8d9ffe47d902dca..a5bb1b41c8fbd8d8f62b8b7718fce150e5df30ec 100644
--- a/lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala
@@ -89,6 +89,7 @@ trait KernelHelpers {
   given Conversion[VariableLabel, VariableTerm] = VariableTerm.apply
   given Conversion[VariableTerm, VariableLabel] = _.label
   given Conversion[PredicateFormula, PredicateLabel] = _.label
+  given Conversion[PredicateLabel, Formula] = _.apply()
   given Conversion[FunctionTerm, FunctionLabel] = _.label
   given Conversion[SchematicFunctionLabel, Term] = _.apply()
   given Conversion[VariableFormulaLabel, PredicateFormula] = PredicateFormula.apply(_, Nil)
diff --git a/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala b/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala
index d19514fbf8b4e353f501fb0108050025a1c32f6f..33f62829dfcd6905417bc6592845310c925ff59f 100644
--- a/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala
+++ b/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala
@@ -28,17 +28,17 @@ class PrinterTest extends AnyFunSuite {
     assert(prettyFormula(ConnectorFormula(Neg, Seq(ConnectorFormula(Neg, Seq(ConnectorFormula(And, Seq(a, b))))))) == "¬¬(a ∧ b)")
     assert(prettyFormula(ConnectorFormula(And, Seq(ConnectorFormula(Neg, Seq(a)), ConnectorFormula(And, Seq(ConnectorFormula(Neg, Seq(b)), ConnectorFormula(Neg, Seq(c))))))) == "¬a ∧ ¬b ∧ ¬c")
 
-    assert(prettyFormula(ConnectorFormula(And, Seq(a, PredicateFormula(equality, Seq(x, x))))) == "a ∧ (x = x)")
+    assert(prettyFormula(ConnectorFormula(And, Seq(a, PredicateFormula(equality, Seq(x, x))))) == "a ∧ (?x = ?x)")
 
-    assert(prettyFormula(BinderFormula(Forall, x, PredicateFormula(equality, Seq(x, x)))) == "∀x. x = x")
-    assert(prettyFormula(ConnectorFormula(And, Seq(a, BinderFormula(Forall, x, PredicateFormula(equality, Seq(x, x)))))) == "a ∧ ∀x. x = x")
+    assert(prettyFormula(BinderFormula(Forall, x, PredicateFormula(equality, Seq(x, x)))) == "∀x. ?x = ?x")
+    assert(prettyFormula(ConnectorFormula(And, Seq(a, BinderFormula(Forall, x, PredicateFormula(equality, Seq(x, x)))))) == "a ∧ ∀x. ?x = ?x")
     assert(prettyFormula(ConnectorFormula(And, Seq(BinderFormula(Forall, x, b), a))) == "(∀x. b) ∧ a")
     assert(prettyFormula(ConnectorFormula(And, Seq(ConnectorFormula(And, Seq(a, BinderFormula(Forall, x, b))), a))) == "(a ∧ ∀x. b) ∧ a")
     assert(prettyFormula(ConnectorFormula(Or, Seq(ConnectorFormula(And, Seq(a, BinderFormula(Forall, x, b))), a))) == "a ∧ (∀x. b) ∨ a")
 
     assert(prettyFormula(BinderFormula(Forall, x, BinderFormula(Exists, y, BinderFormula(ExistsOne, z, a)))) == "∀x. ∃y. ∃!z. a")
 
-    assert(prettyFormula(PredicateFormula(ConstantPredicateLabel("f", 2), Seq(x, y, z))) == "f(x, y, z)")
+    assert(prettyFormula(PredicateFormula(ConstantPredicateLabel("f", 2), Seq(x, y, z))) == "f(?x, ?y, ?z)")
   }
 
 }