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 c8f99bebd450a6ea83b9857a870adaa49c71b9ad..27f1bcbb57de39a8619b1320f1f3df4c13b33387 100644
--- a/lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaLabelDefinitions.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaLabelDefinitions.scala
@@ -51,7 +51,19 @@ private[fol] trait FormulaLabelDefinitions extends CommonDefinitions {
   /**
    * A predicate symbol that can be instantiated with any formula.
    */
-  sealed case class SchematicPredicateLabel(id: String, arity: Int) extends PredicateLabel
+  sealed abstract class SchematicPredicateLabel extends PredicateLabel with SchematicLabel
+
+  /**
+   * A predicate symbol of non-zero arity that can be instantiated with any formula taking arguments.
+   */
+  sealed case class SchematicNPredicateLabel(id: String, arity: Int) extends SchematicPredicateLabel
+
+  /**
+   * A predicate symbol of arity 0 that can be instantiated with any formula.
+   */
+  sealed case class VariableFormulaLabel(id: String) extends SchematicPredicateLabel {
+    val arity = 0
+  }
 
   /**
    * 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/Substitutions.scala b/lisa-kernel/src/main/scala/lisa/kernel/fol/Substitutions.scala
index cf91986365fefb81fb19866eab87c887a9448bdf..be1d60b3d44e605cd98f876bb35d9061660715c4 100644
--- a/lisa-kernel/src/main/scala/lisa/kernel/fol/Substitutions.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/fol/Substitutions.scala
@@ -31,8 +31,7 @@ trait Substitutions extends FormulaDefinitions {
    * @param vars The names of the "holes" in a formula, necessarily of arity 0.
    * @param body The formula represented by the object, up to instantiation of the bound schematic variables in args.
    */
-  case class LambdaFormulaFormula(vars: Seq[SchematicPredicateLabel], body: Formula) {
-    require(vars.forall(_.arity == 0))
+  case class LambdaFormulaFormula(vars: Seq[VariableFormulaLabel], body: Formula) {
     def apply(args: Seq[Formula]): Formula = instantiatePredicateSchemas(body, (vars zip (args map (LambdaTermFormula(Nil, _)))).toMap)
   }
 
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 c456cc476b4d4b4e9e974808f836adcf877ffdd1..0b9230973fb68cbcaed124b2827d3449998dca6e 100644
--- a/lisa-kernel/src/main/scala/lisa/kernel/fol/TermLabelDefinitions.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/fol/TermLabelDefinitions.scala
@@ -55,7 +55,9 @@ 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
    */
-  sealed case class SchematicFunctionLabel(id: String, arity: Int) extends FunctionLabel with SchematicTermLabel
+  sealed case class SchematicFunctionLabel(id: String, arity: Int) extends FunctionLabel with SchematicTermLabel{
+    require(arity >= 1 && arity < MaxArity)
+  }
 
   /**
    * The label of a term which is a variable.
diff --git a/lisa-theories/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala b/lisa-theories/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala
index f38aa7b1edd8ee07cd64b0cbb1ce565097bbe8d8..ecf2c80c013309ee549d9291eff2374abfa82b4c 100644
--- a/lisa-theories/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala
+++ b/lisa-theories/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala
@@ -11,7 +11,7 @@ private[settheory] trait SetTheoryZAxioms extends SetTheoryDefinitions {
 
   private val (x, y, z) =
     (VariableLabel("x"), VariableLabel("y"), VariableLabel("z"))
-  private final val sPhi = SchematicPredicateLabel("P", 2)
+  private final val sPhi = SchematicNPredicateLabel("P", 2)
 
   final val emptySetAxiom: Formula = forall(x, !in(x, emptySet()))
   final val extensionalityAxiom: Formula = forall(x, forall(y, forall(z, in(z, x) <=> in(z, y)) <=> (x === y)))
diff --git a/lisa-theories/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala b/lisa-theories/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala
index bd95ad4551a1c40f9cf94799a63cba71e1a93a06..e075fabbb9f5fe687ef71cfe859c1c8b5691a51c 100644
--- a/lisa-theories/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala
+++ b/lisa-theories/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala
@@ -9,7 +9,7 @@ import lisa.utils.Helpers.{_, given}
 private[settheory] trait SetTheoryZFAxioms extends SetTheoryZAxioms {
   private val (x, y, a, b) =
     (VariableLabel("x"), VariableLabel("y"), VariableLabel("A"), VariableLabel("B"))
-  private final val sPsi = SchematicPredicateLabel("P", 3)
+  private final val sPsi = SchematicNPredicateLabel("P", 3)
 
   final val replacementSchema: Formula = forall(
     a,
diff --git a/lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala b/lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala
index d574cd63f97bdbea6fbe23f043234b967fc417c3..1452de69e93e7c051afa06c4e8d9ffe47d902dca 100644
--- a/lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala
@@ -91,6 +91,7 @@ trait KernelHelpers {
   given Conversion[PredicateFormula, PredicateLabel] = _.label
   given Conversion[FunctionTerm, FunctionLabel] = _.label
   given Conversion[SchematicFunctionLabel, Term] = _.apply()
+  given Conversion[VariableFormulaLabel, PredicateFormula] = PredicateFormula.apply(_, Nil)
   given Conversion[(Boolean, List[Int], String), Option[(List[Int], String)]] = tr => if (tr._1) None else Some(tr._2, tr._3)
   given Conversion[Formula, Sequent] = () |- _
 
diff --git a/lisa-utils/src/main/scala/lisa/utils/Printer.scala b/lisa-utils/src/main/scala/lisa/utils/Printer.scala
index c19f126692a699e4a15b9b2250f2acf8f61f2ec5..fb51c81fe9dfc62ca69f359b6c431c4f248ea2d3 100644
--- a/lisa-utils/src/main/scala/lisa/utils/Printer.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/Printer.scala
@@ -67,7 +67,7 @@ object Printer {
         case _ =>
           val labelString = label match {
             case ConstantPredicateLabel(id, _) => id
-            case SchematicPredicateLabel(id, _) => s"?$id"
+            case s:SchematicPredicateLabel => s"?${s.id}"
           }
           prettyFunction(labelString, args.map(prettyTerm(_, compact)), compact)
       }
diff --git a/lisa-utils/src/test/scala/lisa/kernel/IncorrectProofsTests.scala b/lisa-utils/src/test/scala/lisa/kernel/IncorrectProofsTests.scala
index 786e63add0d36d6b10cd5b3fc4a7ac8876ab0600..d01a59f3518b52ed028bab03f8b506d92241e444 100644
--- a/lisa-utils/src/test/scala/lisa/kernel/IncorrectProofsTests.scala
+++ b/lisa-utils/src/test/scala/lisa/kernel/IncorrectProofsTests.scala
@@ -17,7 +17,7 @@ class IncorrectProofsTests extends ProofCheckerSuite {
     // Shorthand
     implicit def proofStepToProof(proofStep: SCProofStep): SCProof = SCProof(proofStep)
 
-    val (fl, gl, hl) = (SchematicPredicateLabel("f", 0), SchematicPredicateLabel("g", 0), SchematicPredicateLabel("h", 0))
+    val (fl, gl, hl) = (VariableFormulaLabel("f"), VariableFormulaLabel("g"), VariableFormulaLabel("h"))
     val f = PredicateFormula(fl, Seq.empty) // Some arbitrary formulas
     val g = PredicateFormula(gl, Seq.empty)
     val h = PredicateFormula(hl, Seq.empty)
diff --git a/src/main/scala/lisa/proven/mathematics/Mapping.scala b/src/main/scala/lisa/proven/mathematics/Mapping.scala
index a70079678e189c240902b6350829076ffa40861e..707dbce76b4283f1079cb1558312b78728b6d6ff 100644
--- a/src/main/scala/lisa/proven/mathematics/Mapping.scala
+++ b/src/main/scala/lisa/proven/mathematics/Mapping.scala
@@ -14,19 +14,18 @@ object Mapping extends lisa.proven.Main {
     THEOREM("functionalMapping") of
         "∀a. (a ∈ ?A) ⇒ ∃!x. ?phi(x, a) ⊢ ∃!X. ∀x. (x ∈ X) ↔ ∃a. (a ∈ ?A) ∧ ?phi(x, a)" PROOF {
         val a = VariableLabel("a")
-        val b = VariableLabel("b")
         val x = VariableLabel("x")
         val y = VariableLabel("y")
         val z = VariableLabel("z")
         val f = VariableLabel("f")
-        val h = SchematicPredicateLabel("h", 0)
+        val h = VariableFormulaLabel("h")
         val A = VariableLabel("A")
         val X = VariableLabel("X")
         val B = VariableLabel("B")
         val B1 = VariableLabel("B1")
-        val phi = SchematicPredicateLabel("phi", 2)
-        val sPhi = SchematicPredicateLabel("P", 2)
-        val sPsi = SchematicPredicateLabel("P", 3)
+        val phi = SchematicNPredicateLabel("phi", 2)
+        val sPhi = SchematicNPredicateLabel("P", 2)
+        val sPsi = SchematicNPredicateLabel("P", 3)
 
         val H = existsOne(x, phi(x, a))
         val H1 = forall(a, in(a, A) ==> H)
@@ -244,13 +243,13 @@ object Mapping extends lisa.proven.Main {
         val y = VariableLabel("y")
         val z = VariableLabel("z")
         val f = VariableLabel("f")
-        val h = SchematicPredicateLabel("h", 0)
+        val h = VariableFormulaLabel("h")
         val A = VariableLabel("A")
         val X = VariableLabel("X")
         val B = VariableLabel("B")
         val B1 = VariableLabel("B1")
-        val phi = SchematicPredicateLabel("phi", 2)
-        val psi = SchematicPredicateLabel("psi", 3)
+        val phi = SchematicNPredicateLabel("phi", 2)
+        val psi = SchematicNPredicateLabel("psi", 3)
         val H = existsOne(x, phi(x, a))
         val H1 = forall(a, in(a, A) ==> H)
         val i1 = thm"functionalMapping"
@@ -270,7 +269,7 @@ object Mapping extends lisa.proven.Main {
         val s6 = InstFunSchema(
             forall(b, in(b, B) ==> existsOne(X, phi(X, b))) |- instantiateTermSchemas(i1.right.head, Map(A -> LambdaTermTerm(Nil, B))),
             -1,
-            Map(SchematicFunctionLabel("A", 0) -> LambdaTermTerm(Nil, B))
+            Map(A -> LambdaTermTerm(Nil, B))
         )
         val s7 = InstPredSchema(
             forall(b, in(b, B) ==> existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b))))) |- existsOne(
@@ -307,13 +306,13 @@ object Mapping extends lisa.proven.Main {
         val z1 = VariableLabel("z1")
         val F = SchematicFunctionLabel("F", 1)
         val f = VariableLabel("f")
-        val phi = SchematicPredicateLabel("phi", 1)
-        val g = SchematicPredicateLabel("g", 0)
+        val phi = SchematicNPredicateLabel("phi", 1)
+        val g = VariableFormulaLabel("g")
 
         val g2 = SCSubproof({
             val s0 = hypothesis(F(x1) === z)
             val s1 = LeftSubstEq((x === x1, F(x) === z) |- F(x1) === z, 0, List((x, x1)), LambdaTermFormula(Seq(f), F(f) === z))
-            val s2 = LeftSubstIff(Set(phi(x) <=> (x === x1), phi(x), F(x) === z) |- F(x1) === z, 1, List((x === x1, phi(x))), LambdaFormulaFormula(Seq(g), g()))
+            val s2 = LeftSubstIff(Set(phi(x) <=> (x === x1), phi(x), F(x) === z) |- F(x1) === z, 1, List((x === x1, phi(x))), LambdaFormulaFormula(Seq(g), g))
             val s3 = LeftForall(Set(forall(x, phi(x) <=> (x === x1)), phi(x), F(x) === z) |- F(x1) === z, 2, phi(x) <=> (x === x1), x, x)
             val s4 = Rewrite(Set(forall(x, phi(x) <=> (x === x1)), phi(x) /\ (F(x) === z)) |- F(x1) === z, 3)
             val s5 = LeftExists(Set(forall(x, phi(x) <=> (x === x1)), exists(x, phi(x) /\ (F(x) === z))) |- F(x1) === z, 4, phi(x) /\ (F(x) === z), x)
@@ -358,8 +357,8 @@ object Mapping extends lisa.proven.Main {
         val F = SchematicFunctionLabel("F", 1)
         val A = VariableLabel("A")
         val B = VariableLabel("B")
-        val phi = SchematicPredicateLabel("phi", 1)
-        val psi = SchematicPredicateLabel("psi", 3)
+        val phi = SchematicNPredicateLabel("phi", 1)
+        val psi = SchematicNPredicateLabel("psi", 3)
 
         val i1 = thm"lemmaLayeredTwoArgumentsMap"
         val i2 = thm"applyFunctionToUniqueObject"
@@ -403,7 +402,7 @@ object Mapping extends lisa.proven.Main {
             val x = VariableLabel("x")
             val A = VariableLabel("A")
             val B = VariableLabel("B")
-            val psi = SchematicPredicateLabel("psi", 3)
+            val psi = SchematicNPredicateLabel("psi", 3)
 
             val i1 = thm"mapTwoArguments" // ∀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)
 
diff --git a/src/main/scala/lisa/proven/mathematics/SetTheory.scala b/src/main/scala/lisa/proven/mathematics/SetTheory.scala
index 21dffc61297a36b62bee9b16d4541905391b6208..353443915428af8a159d73d6a8f7dbc96b346ae4 100644
--- a/src/main/scala/lisa/proven/mathematics/SetTheory.scala
+++ b/src/main/scala/lisa/proven/mathematics/SetTheory.scala
@@ -24,7 +24,7 @@ object SetTheory extends lisa.proven.Main {
       val x = VariableLabel("x")
       val y = VariableLabel("y")
       val z = VariableLabel("z")
-      val h = SchematicPredicateLabel("h", 0)
+      val h = VariableFormulaLabel("h")
       val fin = SCSubproof(
         {
           val pr0 = SCSubproof(
@@ -47,7 +47,7 @@ object SetTheory extends lisa.proven.Main {
             Sequent(pr1.bot.right, Set(in(z, pair(x, y)) <=> in(z, pair(y, x)))),
             0,
             List(((x === z) \/ (y === z), in(z, pair(y, x)))),
-            LambdaFormulaFormula(Seq(h), in(z, pair(x, y)) <=> h())
+            LambdaFormulaFormula(Seq(h), in(z, pair(x, y)) <=> h)
           )
           val pr3 = Cut(Sequent(pr1.bot.left, pr2.bot.right), 1, 2, pr2.bot.left.head)
           val pr4 = RightForall(Sequent(Set(), Set(forall(z, pr2.bot.right.head))), 3, pr2.bot.right.head, z)
@@ -81,7 +81,7 @@ object SetTheory extends lisa.proven.Main {
       val y1 = VariableLabel("y'")
       val z = VariableLabel("z")
       val g = VariableLabel("g")
-      val h = SchematicPredicateLabel("h", 0)
+      val h = VariableFormulaLabel("h")
       val pxy = pair(x, y)
       val pxy1 = pair(x1, y1)
       val p0 = SCSubproof(
@@ -125,7 +125,7 @@ object SetTheory extends lisa.proven.Main {
             emptySeq +< p3.bot.left.head +< p2.bot.right.head +> (((z === x) \/ (z === y)) <=> ((z === x1) \/ (z === y1))),
             3,
             List(((z === x1) \/ (z === y1), in(z, pxy1))),
-            LambdaFormulaFormula(Seq(h), h() <=> ((z === x) \/ (z === y)))
+            LambdaFormulaFormula(Seq(h), h <=> ((z === x) \/ (z === y)))
           ) //  ((z∈{x',y'})↔((x'=z)∨(y'=z))), ({x,y}={x',y'}) |- (((z=x)∨(z=y))↔((z=x')∨(z=y')))
           val p5 = Cut(emptySeq ++< p3.bot ++> p4.bot, 2, 4, p2.bot.right.head)
           Proof(IndexedSeq(p0, p1, p2, p3, p4, p5), IndexedSeq(() |- pairAxiom))
@@ -172,7 +172,7 @@ object SetTheory extends lisa.proven.Main {
                                 emptySeq +< (pxy === pxy1) +< (x === y) +< (f1 <=> (f1 \/ f1)) +> (f1 <=> ((z === x1) \/ (z === y1))),
                                 1,
                                 List((f1, f1 \/ f1)),
-                                LambdaFormulaFormula(Seq(h), h() <=> ((z === x1) \/ (z === y1)))
+                                LambdaFormulaFormula(Seq(h), h <=> ((z === x1) \/ (z === y1)))
                               )
                               val pa0_3 =
                                 Cut(emptySeq +< (pxy === pxy1) +< (x === y) +> (f1 <=> ((z === x1) \/ (z === y1))), 0, 2, f1 <=> (f1 \/ f1)) //  (x=y), ({x,y}={x',y'}) |- ((z=x)↔((z=x')∨(z=y')))
@@ -275,7 +275,7 @@ object SetTheory extends lisa.proven.Main {
                       pd0_1.bot.right |- ((x1 === x) \/ (x1 === y)),
                       0,
                       List(((x1 === x) \/ (x1 === y), (x1 === x1) \/ (x1 === y1))),
-                      LambdaFormulaFormula(Seq(h), h())
+                      LambdaFormulaFormula(Seq(h), h)
                     ) // (x'=x \/ x'=y) <=> (x'=x' \/ x'=y') |- (x'=x \/ x'=y)
                     val pd0_3 = Cut(pd0_1.bot.left |- pd0_2.bot.right, 1, 2, pd0_1.bot.right.head) //  ({x,y}={x',y'}) |- (x=x' \/ y=x')
                     destructRightOr(Proof(IndexedSeq(pd0_0, pd0_1, pd0_2, pd0_3), IndexedSeq(pd0_m1.bot)), x === x1, y === x1) //  ({x,y}={x',y'}) |- x=x',  y=x'
@@ -333,8 +333,8 @@ object SetTheory extends lisa.proven.Main {
     val x = VariableLabel("x")
     val y = VariableLabel("y")
     val z = VariableLabel("z")
-    val h = SchematicPredicateLabel("h", 0)
-    val sPhi = SchematicPredicateLabel("P", 2)
+    val h = VariableFormulaLabel("h")
+    val sPhi = SchematicNPredicateLabel("P", 2)
     // forall(z, exists(y, forall(x, in(x,y) <=> (in(x,y) /\ sPhi(x,z)))))
     val i1 = () |- comprehensionSchema
     val i2 = thm"russelParadox" // forall(x1, in(x1,y) <=> !in(x1, x1)) |- ()
@@ -345,7 +345,7 @@ object SetTheory extends lisa.proven.Main {
       (in(x, z) <=> And(), in(x, y) <=> (in(x, z) /\ !in(x, x))) |- in(x, y) <=> (And() /\ !in(x, x)),
       1,
       List((in(x, z), And())),
-      LambdaFormulaFormula(Seq(h), in(x, y) <=> (h() /\ !in(x, x)))
+      LambdaFormulaFormula(Seq(h), in(x, y) <=> (h /\ !in(x, x)))
     ) // in(x1,y1) <=> (in(x1,z1) /\ in(x1, x1)) |- in(x,y) <=> (And() /\ in(x1, x1))
     val s3 = Rewrite((in(x, z), in(x, y) <=> (in(x, z) /\ !in(x, x))) |- in(x, y) <=> !in(x, x), 2)
     val s4 = LeftForall((forall(x, in(x, z)), in(x, y) <=> (in(x, z) /\ !in(x, x))) |- in(x, y) <=> !in(x, x), 3, in(x, z), x, x)
diff --git a/src/main/scala/lisa/proven/tactics/SimplePropositionalSolver.scala b/src/main/scala/lisa/proven/tactics/SimplePropositionalSolver.scala
index c48c282d8d2951663a38da9fdd9e8d45895ca25a..65ce706f5723c6d4c5b5d9ac46bb211b81c0093d 100644
--- a/src/main/scala/lisa/proven/tactics/SimplePropositionalSolver.scala
+++ b/src/main/scala/lisa/proven/tactics/SimplePropositionalSolver.scala
@@ -149,7 +149,7 @@ object SimplePropositionalSolver {
 
     } else {
       val f = s.left.find(f => s.right.contains(f))
-      List(Hypothesis(s, if (f.nonEmpty) f.get else PredicateFormula(SchematicPredicateLabel("P", 0), Seq())))
+      List(Hypothesis(s, if (f.nonEmpty) f.get else PredicateFormula(VariableFormulaLabel("P"), Seq())))
     }
   }