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 33f56008205f9078adb84056f5b795ee85b190db..f45ce9117892de9d84b9bb2f66c59de1b73772e3 100644
--- a/lisa-kernel/src/main/scala/lisa/kernel/fol/Substitutions.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/fol/Substitutions.scala
@@ -94,7 +94,7 @@ trait Substitutions extends FormulaDefinitions {
       val newSubst = m - bound
       val fv = m.values.flatMap(_.freeVariables).toSet
       if (fv.contains(bound)) {
-        val newBoundVariable = VariableLabel(freshId(fv.map(_.name), bound.name))
+        val newBoundVariable = VariableLabel(freshId(fv.map(_.name) ++ m.keys.map(_.id), bound.name))
         val newInner = substituteVariables(inner, Map(bound -> VariableTerm(newBoundVariable)))
         BinderFormula(label, newBoundVariable, substituteVariables(newInner, newSubst))
       } else BinderFormula(label, bound, substituteVariables(inner, newSubst))
@@ -136,7 +136,7 @@ trait Substitutions extends FormulaDefinitions {
         val newSubst = m - bound
         val fv: Set[VariableLabel] = newSubst.flatMap { case (symbol, LambdaTermTerm(arguments, body)) => body.freeVariables }.toSet
         if (fv.contains(bound)) {
-          val newBoundVariable = VariableLabel(freshId(fv.map(_.name), bound.name))
+          val newBoundVariable = VariableLabel(freshId(fv.map(_.name) ++ m.keys.map(_.id), bound.name))
           val newInner = substituteVariables(inner, Map(bound -> VariableTerm(newBoundVariable)))
           BinderFormula(label, newBoundVariable, instantiateTermSchemas(newInner, newSubst))
         } else BinderFormula(label, bound, instantiateTermSchemas(inner, newSubst))
@@ -232,7 +232,7 @@ trait Substitutions extends FormulaDefinitions {
             (mPred.flatMap { case (symbol, LambdaTermFormula(arguments, body)) => body.freeVariables }).toSet ++
             (mTerm.flatMap { case (symbol, LambdaTermTerm(arguments, body)) => body.freeVariables }).toSet
         if (fv.contains(bound)) {
-          val newBoundVariable = VariableLabel(freshId(fv.map(_.name), bound.name))
+          val newBoundVariable = VariableLabel(freshId(fv.map(_.name) ++ mTerm.keys.map(_.id), bound.name))
           val newInner = substituteVariables(inner, Map(bound -> VariableTerm(newBoundVariable)))
           BinderFormula(label, newBoundVariable, instantiateSchemas(newInner, mCon, mPred, newmTerm))
         } else BinderFormula(label, bound, instantiateSchemas(inner, mCon, mPred, newmTerm))
diff --git a/lisa-utils/src/test/scala/lisa/kernel/SubstitutionTest.scala b/lisa-utils/src/test/scala/lisa/kernel/SubstitutionTest.scala
index 19c4b39c970f4d7bdcf656caef9b8536c37ec331..901d685103b68c9cb36459db9df77e318fa02f05 100644
--- a/lisa-utils/src/test/scala/lisa/kernel/SubstitutionTest.scala
+++ b/lisa-utils/src/test/scala/lisa/kernel/SubstitutionTest.scala
@@ -13,6 +13,7 @@ import org.scalatest.funsuite.AnyFunSuite
 
 class SubstitutionTest extends AnyFunSuite {
   private val x = variable
+  private val x1 = VariableLabel(Identifier("x", 1))
   private val x2 = variable
   private val x3 = variable
   private val y = variable
@@ -85,6 +86,7 @@ class SubstitutionTest extends AnyFunSuite {
       $(Q(f(f(h(x, y)))) /\ R(x, h(y, f(z))), x -> z(), h -> lambda(Seq(x, z), g(h(z, y))), z -> y()) _VS_ Q(f(f(g(h(y, y))))) /\ R(z, g(h(f(y), y))),
       $(forall(x, R(x, y)), x -> z()) _VS_ forall(x, R(x, y)),
       $(forall(x, R(x, y)), y -> z()) _VS_ forall(x, R(x, z)),
+      $(forall(x, P(x)), x1 -> f(x())) _VS_ forall(x, P(x)),
       $(forall(x, R(x, y)) /\ P(h(x, y)), y -> z(), x -> y()) _VS_ forall(x, R(x, z)) /\ P(h(y, z)),
       $(forall(x, R(x, y)) /\ P(h(x, y)), y -> x()) _VS_ forall(y, R(y, x)) /\ P(h(x, x)),
       $(existsOne(x, R(x, y)) /\ P(h(x, y)), y -> x()) _VS_ existsOne(y, R(y, x)) /\ P(h(x, x))
@@ -214,6 +216,7 @@ class SubstitutionTest extends AnyFunSuite {
         X -> (z === y),
         P -> lambda(x2, exists(y, R(x2, y) /\ P(x)))
       ) _VS_ (exists(y2, Q(y2) /\ ((z === y) <=> exists(x2, P(x2) /\ exists(y, R(x, y) /\ P(x))))) /\ R(y, f(y))),
+      $(forall(x, P(x)), x1 -> f(x())) _VS_ forall(x, P(x)),
       $(
         forall(x, e2(c1(e2(X, P(x))) /\ R(y, f(y)), exists(x, P(x) /\ X))),
         c1 -> lambda(X, exists(y, Q(y) /\ X)),