diff --git a/src/main/scala/lisa/kernel/fol/CommonDefinitions.scala b/src/main/scala/lisa/kernel/fol/CommonDefinitions.scala
index 65906e987404b68b249b1056434a26e2897e501e..c701d239bfcd346a57ea611231aee7626a8e1727 100644
--- a/src/main/scala/lisa/kernel/fol/CommonDefinitions.scala
+++ b/src/main/scala/lisa/kernel/fol/CommonDefinitions.scala
@@ -21,9 +21,15 @@ private[fol] trait CommonDefinitions {
   }
 
   /**
-   * Marks classes that can represent symbols in a theory
+   * Constant label can represent a symbol of a theory
    */
-  trait TheorySymbol
+  trait ConstantLabel extends Label
+
+  /**
+   * Schematic label in a formula can be substituted by any constant label of the respective
+   * kind (predicate or function)
+   */
+  trait SchematicLabel extends Label
 
   def freshId(taken: Set[String], base: String): String = {
     var i = 0;
diff --git a/src/main/scala/lisa/kernel/fol/FormulaLabelDefinitions.scala b/src/main/scala/lisa/kernel/fol/FormulaLabelDefinitions.scala
index 3439bc0ae1887e6908dc63bce6aa091718078dcb..1f40fb69ead8d53a7974fa87a5839441e554cf0b 100644
--- a/src/main/scala/lisa/kernel/fol/FormulaLabelDefinitions.scala
+++ b/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 TheorySymbol
+  final case class ConstantPredicateLabel(id: String, arity: Int) extends PredicateLabel with ConstantLabel
 
   /**
    * The equality symbol (=) for first order logic.
diff --git a/src/main/scala/lisa/kernel/fol/TermLabelDefinitions.scala b/src/main/scala/lisa/kernel/fol/TermLabelDefinitions.scala
index 24c501dce518654244c15ceb3562e85dd3696c53..c08080f2119263af321ac2d9a3cb3b582ff7245b 100644
--- a/src/main/scala/lisa/kernel/fol/TermLabelDefinitions.scala
+++ b/src/main/scala/lisa/kernel/fol/TermLabelDefinitions.scala
@@ -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 TheorySymbol
+  final case class ConstantFunctionLabel(id: String, arity: Int) extends FunctionLabel with ConstantLabel
 
   /**
    * A schematic function symbol that can be substituted.
diff --git a/src/main/scala/lisa/kernel/proof/RunningTheory.scala b/src/main/scala/lisa/kernel/proof/RunningTheory.scala
index 15175569f99403ed26236b9d7f4cfb1cbab7e3ed..6364970e0370078da76dfdb76cf08408d6bf43fe 100644
--- a/src/main/scala/lisa/kernel/proof/RunningTheory.scala
+++ b/src/main/scala/lisa/kernel/proof/RunningTheory.scala
@@ -62,12 +62,12 @@ 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[TheorySymbol, Option[Definition]] = mMap(equality -> None)
+  private[proof] val definitions: mMap[ConstantLabel, Option[Definition]] = mMap(equality -> None)
 
   /**
    * Check if a label is a symbol of the theory
    */
-  def isSymbol(label: TheorySymbol): Boolean = definitions.contains(label)
+  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.
@@ -255,13 +255,13 @@ 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: TheorySymbol): Unit = definitions.update(s, None)
+  def addSymbol(s: ConstantLabel): Unit = definitions.update(s, 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[(TheorySymbol, Option[Definition])] = definitions.toList
+  def language: List[(ConstantLabel, Option[Definition])] = definitions.toList
 
   /**
    * Public accessor to the current set of axioms of the theory