diff --git a/src/main/scala/lisa/kernel/Printer.scala b/src/main/scala/lisa/kernel/Printer.scala
index f367a551bade5d3d7904cf35eb1a3e63c5e35d34..6f27c597e980e9b2eaa4b6ba79ea9c7e6f5aaa12 100644
--- a/src/main/scala/lisa/kernel/Printer.scala
+++ b/src/main/scala/lisa/kernel/Printer.scala
@@ -258,8 +258,8 @@ object Printer {
                             case RightSubstEq(_, t1, _, _, _, _) => pretty("R. SubstEq", t1)
                             case LeftSubstIff(_, t1, _, _, _, _) => pretty("L. SubstIff", t1)
                             case RightSubstIff(_, t1, _, _, _, _) => pretty("R. SubstIff", t1)
-                            case InstantiateSchematicFunction(_, t1, _, _, _) => pretty("?Fun Instantiation", t1)
-                            case InstantiateSchematicPredicate(_, t1, _, _, _) => pretty("?Pred Instantiation", t1)
+                            case InstFunSchema(_, t1, _, _, _) => pretty("?Fun Instantiation", t1)
+                            case InstPredSchema(_, t1, _, _, _) => pretty("?Pred Instantiation", t1)
                             case SCSubproof(_, _, false) => pretty("SCSubproof (hidden)")
                             case other => throw new Exception(s"No available method to print this proof step, consider updating Printer.scala\n$other")
                         }
diff --git a/src/main/scala/lisa/kernel/proof/SCProofChecker.scala b/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
index f2e55a7ed4e5729b1fa0be48696bad0a10d56aab..11fd361ef0fb440dbc07828fa64b5fdc4f7422b2 100644
--- a/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
+++ b/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
@@ -403,12 +403,12 @@ object SCProofChecker {
                     else (false, Nil, "Predicate schema ?q must have arity 0.")
                 /**
                  * <pre>
-                 *    Γ |- Δ
-                 * ---------------------
-                 *  Γ[?f/r(a)] |- Δ[?f/r(a)]
+                 *           Γ |- Δ
+                 * --------------------------
+                 *  Γ[r(a)/?f] |- Δ[r(a)/?f]
                  * </pre>
                  */
-                case InstantiateSchematicFunction(bot, t1, f, r, a) =>
+                case InstFunSchema(bot, t1, f, r, a) =>
                     val expected = (ref(t1).left.map(phi => instantiateFunctionSchema(phi, f, r, a)), ref(t1).right.map(phi => instantiateFunctionSchema(phi, f, r, a)))
                     if (isSameSet(bot.left, expected._1))
                         if (isSameSet(bot.right, expected._2))
@@ -418,12 +418,12 @@ object SCProofChecker {
 
                 /**
                  * <pre>
-                 *    Γ |- Δ
-                 * ---------------------
-                 *  Γ[?p/ψ(a)] |- Δ[?p/ψ(a)]
+                 *           Γ |- Δ
+                 * --------------------------
+                 *  Γ[ψ(a)/?p] |- Δ[ψ(a)/?p]
                  * </pre>
                  */
-                case InstantiateSchematicPredicate(bot, t1, p, psi, a) =>
+                case InstPredSchema(bot, t1, p, psi, a) =>
                     val expected = (ref(t1).left.map(phi => instantiatePredicateSchema(phi, p, psi, a)), ref(t1).right.map(phi => instantiatePredicateSchema(phi, p, psi, a)))
                     if (isSameSet(bot.left, expected._1))
                         if (isSameSet(bot.right, expected._2))
diff --git a/src/main/scala/lisa/kernel/proof/SequentCalculus.scala b/src/main/scala/lisa/kernel/proof/SequentCalculus.scala
index 31fd15c5f9b2880b658aed58f68870e38e126297..5c1470c96a5535899cd8a828835a3128ec1e6fe1 100644
--- a/src/main/scala/lisa/kernel/proof/SequentCalculus.scala
+++ b/src/main/scala/lisa/kernel/proof/SequentCalculus.scala
@@ -279,20 +279,20 @@ object SequentCalculus {
     case class RightSubstIff(bot: Sequent, t1: Int, fa: Formula, fb: Formula, phi: Formula, h: SchematicPredicateLabel) extends SCProofStep{val premises = Seq(t1)}
     /**
      * <pre>
-     *    Γ |- Δ
-     * ---------------------
+     *           Γ |- Δ
+     * --------------------------
      *  Γ[r(a)/?f] |- Δ[r(a)/?f]
      * </pre>
      */
-    case class InstantiateSchematicFunction(bot:Sequent, t1:Int, f:SchematicFunctionLabel, r:Term, a: Seq[VariableLabel] )
+    case class InstFunSchema(bot:Sequent, t1:Int, f:SchematicFunctionLabel, r:Term, a: Seq[VariableLabel] )
     /**
      * <pre>
-     *    Γ |- Δ
-     * ---------------------
+     *           Γ |- Δ
+     * --------------------------
      *  Γ[ψ(a)/?p] |- Δ[ψ(a)/?p]
      * </pre>
      */
-    case class InstantiateSchematicPredicate(bot:Sequent, t1:Int, p:SchematicPredicateLabel, psi:Formula, a: Seq[VariableLabel] )
+    case class InstPredSchema(bot:Sequent, t1:Int, p:SchematicPredicateLabel, psi:Formula, a: Seq[VariableLabel] )
 
     // Proof Organisation rules
     case class SCSubproof(sp: SCProof, premises: Seq[Int] = Seq.empty, display:Boolean = true) extends SCProofStep {