diff --git a/LISA Reference Manual.pdf b/LISA Reference Manual.pdf
index 906435e4e6b5d7fcd132c57896cf07d86704556e..a4f64cbc8843cd905e63b0b863119832574abcc8 100644
Binary files a/LISA Reference Manual.pdf and b/LISA Reference Manual.pdf differ
diff --git a/src/main/scala/lisa/kernel/proof/SequentCalculus.scala b/src/main/scala/lisa/kernel/proof/SequentCalculus.scala
index 7dce18204a55474b2a23154f09d012b0d2a85b51..31fd15c5f9b2880b658aed58f68870e38e126297 100644
--- a/src/main/scala/lisa/kernel/proof/SequentCalculus.scala
+++ b/src/main/scala/lisa/kernel/proof/SequentCalculus.scala
@@ -263,17 +263,17 @@ object SequentCalculus {
     case class RightSubstEq(bot: Sequent, t1: Int, s: Term, t: Term, phi: Formula, f: SchematicFunctionLabel) extends SCProofStep{val premises = Seq(t1)}
     /**
      * <pre>
-     *    Γ, φ[a/h] |- Δ
+     *    Γ, φ[a/?p] |- Δ
      * ---------------------
-     *  Γ, a↔b, φ[b/h] |- Δ
+     *  Γ, a↔b, φ[b/?p] |- Δ
      * </pre>
      */
     case class LeftSubstIff(bot: Sequent, t1: Int, fa: Formula, fb: Formula, phi: Formula, h: SchematicPredicateLabel) extends SCProofStep{val premises = Seq(t1)}
     /**
      * <pre>
-     *    Γ |- φ[a/h], Δ
+     *    Γ |- φ[a/?p], Δ
      * ---------------------
-     *  Γ, a↔b |- φ[b/h], Δ
+     *  Γ, a↔b |- φ[b/?p], Δ
      * </pre>
      */
     case class RightSubstIff(bot: Sequent, t1: Int, fa: Formula, fb: Formula, phi: Formula, h: SchematicPredicateLabel) extends SCProofStep{val premises = Seq(t1)}
@@ -281,7 +281,7 @@ object SequentCalculus {
      * <pre>
      *    Γ |- Δ
      * ---------------------
-     *  Γ[?f/r(a)] |- Δ[?f/r(a)]
+     *  Γ[r(a)/?f] |- Δ[r(a)/?f]
      * </pre>
      */
     case class InstantiateSchematicFunction(bot:Sequent, t1:Int, f:SchematicFunctionLabel, r:Term, a: Seq[VariableLabel] )
@@ -289,7 +289,7 @@ object SequentCalculus {
      * <pre>
      *    Γ |- Δ
      * ---------------------
-     *  Γ[?p/ψ(a)] |- Δ[?p/ψ(a)]
+     *  Γ[ψ(a)/?p] |- Δ[ψ(a)/?p]
      * </pre>
      */
     case class InstantiateSchematicPredicate(bot:Sequent, t1:Int, p:SchematicPredicateLabel, psi:Formula, a: Seq[VariableLabel] )