Subst syntax change

epfl-lara · Aug 14, 2023 · 2e60437 · 2e60437
1 parent 57c5f91
commit 2e60437
Show file tree

Hide file tree

Showing 8 changed files with 103 additions and 106 deletions.
diff --git a/src/main/scala/lisa/mathematics/fol/Quantifiers.scala b/src/main/scala/lisa/mathematics/fol/Quantifiers.scala
@@ -364,7 +364,7 @@ object Quantifiers extends lisa.Main {
   ) {
     val fwd = have((exists(x, P(x)) /\ !existsOne(x, P(x))) ==> exists(x, exists(y, P(x) /\ P(y) /\ !(x === y)))) subproof {
       have((P(x), ((x === y) /\ !P(y))) |- P(x) /\ !P(y)) by Restate
-      thenHave((P(x), ((x === y) /\ !P(y))) |- P(y) /\ !P(y)) by Substitution.apply2(false, x === y) // contradiction
+      thenHave((P(x), ((x === y) /\ !P(y))) |- P(y) /\ !P(y)) by Substitution.withExplicitRules(x === y) // contradiction
       val xy = thenHave((P(x), ((x === y) /\ !P(y))) |- exists(x, exists(y, P(x) /\ P(y) /\ !(x === y)))) by Weakening
 
       have((P(x), (!(x === y) /\ P(y))) |- (!(x === y) /\ P(y) /\ P(x))) by Restate
@@ -384,7 +384,7 @@ object Quantifiers extends lisa.Main {
       val ex = thenHave((P(x), P(y), !(x === y)) |- exists(x, P(x))) by RightExists
 
       have((P(x), P(y), !(x === y)) |- P(y) /\ !(y === x)) by Restate
-      thenHave((P(x), P(y), !(x === y), (x === z)) |- P(y) /\ !(y === z)) by Substitution.apply2(false, x === z)
+      thenHave((P(x), P(y), !(x === y), (x === z)) |- P(y) /\ !(y === z)) by Substitution.withExplicitRules(x === z)
       thenHave((P(x), P(y), !(x === y), (x === z)) |- (P(y) /\ !(y === z)) \/ (!P(y) /\ (y === z))) by Weakening
       val xz = thenHave((P(x), P(y), !(x === y), (x === z)) |- exists(y, (P(y) /\ !(y === z)) \/ (!P(y) /\ (y === z)))) by RightExists
 

diff --git a/src/main/scala/lisa/mathematics/settheory/SetTheory.scala b/src/main/scala/lisa/mathematics/settheory/SetTheory.scala
@@ -856,11 +856,11 @@ object SetTheory extends lisa.Main {
 
     // but x \cap u contains y, and y \cap u contains x
     have(in(x, u) /\ in(x, y)) by Tautology.from(firstElemInPair)
-    thenHave((z === y) |- in(x, u) /\ in(x, z)) by Substitution.apply2(true, z === y)
+    thenHave((z === y) |- in(x, u) /\ in(x, z)) by Substitution.withExplicitRules(z === y)
     val zy = thenHave((z === y) |- exists(t, in(t, u) /\ in(t, z))) by RightExists
 
     have(in(y, u) /\ in(y, x)) by Tautology.from(secondElemInPair)
-    thenHave((z === x) |- in(y, u) /\ in(y, z)) by Substitution.apply2(true, z === x)
+    thenHave((z === x) |- in(y, u) /\ in(y, z)) by Substitution.withExplicitRules(z === x)
     val zx = thenHave((z === x) |- exists(t, in(t, u) /\ in(t, z))) by RightExists
 
     // this is a contradiction
@@ -2251,7 +2251,7 @@ object SetTheory extends lisa.Main {
     }
 
     val relS = have(relation(s)) subproof {
-      have((z === pair(x, y)) |- in(z, cartesianProduct(singleton(x), singleton(y)))) by Substitution.apply2(true, z === pair(x, y))(xyInCart)
+      have((z === pair(x, y)) |- in(z, cartesianProduct(singleton(x), singleton(y)))) by Substitution.withExplicitRules(z === pair(x, y))(xyInCart)
       have(in(z, s) ==> in(z, cartesianProduct(singleton(x), singleton(y)))) by Tautology.from(lastStep, elemOfS)
       thenHave(forall(z, in(z, s) ==> in(z, cartesianProduct(singleton(x), singleton(y))))) by RightForall
       have(relationBetween(s, singleton(x), singleton(y))) by Tautology.from(
@@ -2266,7 +2266,7 @@ object SetTheory extends lisa.Main {
 
     val uniq = have(forall(a, exists(b, in(pair(a, b), s)) ==> existsOne(b, in(pair(a, b), s)))) subproof {
       have((pair(a, z) === pair(x, y)) <=> in(pair(a, z), s)) by Restate.from(elemOfS of z -> pair(a, z))
-      val eq = thenHave(((a === x) /\ (z === y)) <=> in(pair(a, z), s)) by Substitution.apply2(false, pairExtensionality of (a -> a, b -> z, c -> x, d -> y))
+      val eq = thenHave(((a === x) /\ (z === y)) <=> in(pair(a, z), s)) by Substitution.withExplicitRules(pairExtensionality of (a -> a, b -> z, c -> x, d -> y))
       thenHave((a === x) |- (z === y) <=> in(pair(a, z), s)) by Tautology
       thenHave((a === x) |- forall(z, (z === y) <=> in(pair(a, z), s))) by RightForall
       thenHave((a === x) |- exists(b, forall(z, (z === b) <=> in(pair(a, z), s)))) by RightExists
@@ -2287,7 +2287,7 @@ object SetTheory extends lisa.Main {
       have(forall(t, in(t, relationDomain(s)) <=> exists(a, in(pair(t, a), s)))) by InstantiateForall(relationDomain(s))(relationDomain.definition of r -> s)
       val inDom = thenHave(in(t, relationDomain(s)) <=> exists(a, in(pair(t, a), s))) by InstantiateForall(t)
 
-      have(in(pair(t, a), s) <=> ((t === x) /\ (a === y))) by Substitution.apply2(false, pairExtensionality of (a -> t, b -> a, c -> x, d -> y))(elemOfS of z -> pair(t, a))
+      have(in(pair(t, a), s) <=> ((t === x) /\ (a === y))) by Substitution.withExplicitRules(pairExtensionality of (a -> t, b -> a, c -> x, d -> y))(elemOfS of z -> pair(t, a))
       thenHave(forall(a, in(pair(t, a), s) <=> ((t === x) /\ (a === y)))) by RightForall
       val exToEq = have(exists(a, in(pair(t, a), s)) <=> exists(a, ((t === x) /\ (a === y)))) by Cut(
         lastStep,
@@ -2314,7 +2314,7 @@ object SetTheory extends lisa.Main {
       have(forall(t, in(t, relationRange(s)) <=> exists(a, in(pair(a, t), s)))) by InstantiateForall(relationRange(s))(relationRange.definition of r -> s)
       val inDom = thenHave(in(t, relationRange(s)) <=> exists(a, in(pair(a, t), s))) by InstantiateForall(t)
 
-      have(in(pair(a, t), s) <=> ((a === x) /\ (t === y))) by Substitution.apply2(false, pairExtensionality of (a -> a, b -> t, c -> x, d -> y))(elemOfS of z -> pair(a, t))
+      have(in(pair(a, t), s) <=> ((a === x) /\ (t === y))) by Substitution.withExplicitRules(pairExtensionality of (a -> a, b -> t, c -> x, d -> y))(elemOfS of z -> pair(a, t))
       thenHave(forall(a, in(pair(a, t), s) <=> ((a === x) /\ (t === y)))) by RightForall
       val exToEq = have(exists(a, in(pair(a, t), s)) <=> exists(a, ((a === x) /\ (t === y)))) by Cut(
         lastStep,
@@ -2508,7 +2508,7 @@ object SetTheory extends lisa.Main {
 
     val domEQ = have(relationDomain(f) === x) by Tautology.from(functionalOver.definition)
     have(in(a, x)) by Restate
-    thenHave(in(a, relationDomain(f))) by Substitution.apply2(true, domEQ)
+    thenHave(in(a, relationDomain(f))) by Substitution.withExplicitRules(domEQ)
 
     have(thesis) by Tautology.from(lastStep, functionalOver.definition, pairInFunctionIsApp)
   }
@@ -3449,7 +3449,7 @@ object SetTheory extends lisa.Main {
       val inRan = thenHave((in(b, ran) <=> exists(a, in(pair(a, b), z)))) by InstantiateForall(b)
 
       have((in(t, z)) |- in(t, z)) by Restate
-      val abz = thenHave((in(t, z), (t === pair(a, b))) |- in(pair(a, b), z)) by Substitution.apply2(false, t === pair(a, b))
+      val abz = thenHave((in(t, z), (t === pair(a, b))) |- in(pair(a, b), z)) by Substitution.withExplicitRules(t === pair(a, b))
 
       val exa = have((in(t, z), (t === pair(a, b))) |- exists(a, in(pair(a, b), z))) by RightExists(abz)
       val exb = have((in(t, z), (t === pair(a, b))) |- exists(b, in(pair(a, b), z))) by RightExists(abz)

diff --git a/src/main/scala/lisa/mathematics/settheory/orderings/InclusionOrders.scala b/src/main/scala/lisa/mathematics/settheory/orderings/InclusionOrders.scala
@@ -79,7 +79,7 @@ object InclusionOrders extends lisa.Main {
         val pairExt = have((pair(b, c) === pair(y, x)) |- (b === y) /\ (c === x)) by Weakening(pairExtensionality of (a -> b, b -> c, c -> y, d -> x))
 
         have(in(y, x) |- in(y, x)) by Hypothesis
-        thenHave((in(y, x), b === y, c === x) |- in(b, c)) by Substitution.apply2(true, b === y, c === x)
+        thenHave((in(y, x), b === y, c === x) |- in(b, c)) by Substitution.withExplicitRules(b === y, c === x)
         have((in(y, x) /\ (pair(b, c) === pair(y, x))) |- in(b, c)) by Tautology.from(pairExt, lastStep)
         thenHave(exists(x, in(y, x) /\ (pair(b, c) === pair(y, x))) |- in(b, c)) by LeftExists
         thenHave(thesis) by LeftExists
@@ -105,7 +105,7 @@ object InclusionOrders extends lisa.Main {
     thenHave(in(t, inclusionOn(a)) ==> in(t, cartesianProduct(a, a))) by Weakening
     thenHave(forall(t, in(t, inclusionOn(a)) ==> in(t, cartesianProduct(a, a)))) by RightForall
     // thenHave(forall(z, in(z, inclusionOn(a)) ==> in(z, cartesianProduct(a, a)))) by Restate
-    val subs = thenHave(subset(inclusionOn(a), cartesianProduct(a, a))) by Substitution.apply2(true, subsetAxiom of (x -> inclusionOn(a), y -> cartesianProduct(a, a)))
+    val subs = thenHave(subset(inclusionOn(a), cartesianProduct(a, a))) by Substitution.withExplicitRules(subsetAxiom of (x -> inclusionOn(a), y -> cartesianProduct(a, a)))
 
     have(thesis) by Tautology.from(subs, relationBetween.definition of (r -> inclusionOn(a), a -> a, b -> a))
   }
@@ -156,7 +156,7 @@ object InclusionOrders extends lisa.Main {
     () |- reflexive(inclusionOn(emptySet()), emptySet())
   ) {
     have(reflexive(emptySet(), emptySet())) by Restate.from(emptyRelationReflexiveOnItself)
-    thenHave(thesis) by Substitution.apply2(true, emptySetInclusionEmpty)
+    thenHave(thesis) by Substitution.withExplicitRules(emptySetInclusionEmpty)
   }
 
   /**
@@ -166,7 +166,7 @@ object InclusionOrders extends lisa.Main {
     () |- irreflexive(inclusionOn(emptySet()), a)
   ) {
     have(irreflexive(emptySet(), a)) by Restate.from(emptyRelationIrreflexive)
-    thenHave(thesis) by Substitution.apply2(true, emptySetInclusionEmpty)
+    thenHave(thesis) by Substitution.withExplicitRules(emptySetInclusionEmpty)
   }
 
   /**
@@ -176,7 +176,7 @@ object InclusionOrders extends lisa.Main {
     () |- transitive(inclusionOn(emptySet()), a)
   ) {
     have(transitive(emptySet(), a)) by Restate.from(emptyRelationTransitive)
-    thenHave(thesis) by Substitution.apply2(true, emptySetInclusionEmpty)
+    thenHave(thesis) by Substitution.withExplicitRules(emptySetInclusionEmpty)
   }
 
   /**
@@ -190,7 +190,7 @@ object InclusionOrders extends lisa.Main {
         emptySet(),
         emptySet()
       ) /\ transitive(emptySet(), emptySet()))
-    ) by Substitution.apply2(false, firstInPairReduction of (x -> emptySet(), y -> emptySet()), secondInPairReduction of (x -> emptySet(), y -> emptySet()))(
+    ) by Substitution.withExplicitRules(firstInPairReduction of (x -> emptySet(), y -> emptySet()), secondInPairReduction of (x -> emptySet(), y -> emptySet()))(
       partialOrder.definition of p -> pair(emptySet(), emptySet())
     )
     have(thesis) by Tautology.from(
@@ -208,8 +208,7 @@ object InclusionOrders extends lisa.Main {
   val emptySetTotalOrder = Lemma(
     () |- totalOrder(pair(emptySet(), emptySet()))
   ) {
-    have(totalOrder(pair(emptySet(), emptySet())) <=> (partialOrder(pair(emptySet(), emptySet())) /\ total(emptySet(), emptySet()))) by Substitution.apply2(
-      false,
+    have(totalOrder(pair(emptySet(), emptySet())) <=> (partialOrder(pair(emptySet(), emptySet())) /\ total(emptySet(), emptySet()))) by Substitution.withExplicitRules(
       firstInPairReduction of (x -> emptySet(), y -> emptySet()),
       secondInPairReduction of (x -> emptySet(), y -> emptySet())
     )(totalOrder.definition of p -> pair(emptySet(), emptySet()))

diff --git a/src/main/scala/lisa/mathematics/settheory/orderings/Induction.scala b/src/main/scala/lisa/mathematics/settheory/orderings/Induction.scala
@@ -157,7 +157,7 @@ object Induction extends lisa.Main {
             // well order is anti reflexive
             assume(y === w)
             have(in(pair(w, y), `<p`)) by Restate
-            val ww = thenHave(in(pair(w, w), `<p`)) by Substitution.apply2(false, y === w)
+            val ww = thenHave(in(pair(w, w), `<p`)) by Substitution.withExplicitRules(y === w)
 
             have(∀(y, in(y, A) ==> !in(pair(y, y), `<p`))) subproof {
               have(antiReflexive(`<p`, A)) by Tautology.from(wellOrder.definition, totalOrder.definition, partialOrder.definition)

diff --git a/src/main/scala/lisa/mathematics/settheory/orderings/Ordinals.scala b/src/main/scala/lisa/mathematics/settheory/orderings/Ordinals.scala
@@ -86,8 +86,8 @@ object Ordinals extends lisa.Main {
     () |- wellOrder(inclusionOrderOn(emptySet()))
   ) {
     val incDef = have(inclusionOrderOn(emptySet()) === pair(emptySet(), inclusionOn(emptySet()))) by InstantiateForall(inclusionOrderOn(emptySet()))(inclusionOrderOn.definition of a -> emptySet())
-    have(wellOrder(pair(emptySet(), inclusionOn(emptySet())))) by Substitution.apply2(true, emptySetInclusionEmpty)(emptySetWellOrder)
-    thenHave(thesis) by Substitution.apply2(true, incDef)
+    have(wellOrder(pair(emptySet(), inclusionOn(emptySet())))) by Substitution.withExplicitRules(emptySetInclusionEmpty)(emptySetWellOrder)
+    thenHave(thesis) by Substitution.withExplicitRules(incDef)
   }
 
   /**
@@ -105,7 +105,7 @@ object Ordinals extends lisa.Main {
     val ordinalTrans = have(ordinal(a) |- transitiveSet(a)) by Weakening(ordinal.definition)
     val wellOrdInca = have(ordinal(a) |- wellOrder(inclusionOrderOn(a))) by Weakening(ordinal.definition)
     have(inclusionOrderOn(a) === pair(a, inclusionOn(a))) by InstantiateForall(inclusionOrderOn(a))(inclusionOrderOn.definition)
-    val wellOrda = have(ordinal(a) |- wellOrder(pair(a, inclusionOn(a)))) by Substitution.apply2(false, lastStep)(wellOrdInca)
+    val wellOrda = have(ordinal(a) |- wellOrder(pair(a, inclusionOn(a)))) by Substitution.withExplicitRules(lastStep)(wellOrdInca)
 
     have(transitiveSet(a) |- forall(b, in(b, a) ==> subset(b, a))) by Weakening(transitiveSet.definition of x -> a)
     val bIna = thenHave((transitiveSet(a), in(b, a)) |- subset(b, a)) by InstantiateForall(b)
@@ -119,7 +119,7 @@ object Ordinals extends lisa.Main {
       val bc = have(in(pair(c, b), inclusionOn(a)) |- in(b, a) /\ in(c, a) /\ in(c, b)) by Weakening(inclusionOrderElem of (c -> b, b -> c))
 
       have(wellOrder(pair(a, inclusionOn(a))) |- forall(w, forall(y, forall(z, (in(pair(w, y), inclusionOn(a)) /\ in(pair(y, z), inclusionOn(a))) ==> in(pair(w, z), inclusionOn(a)))))) by Substitution
-        .apply2(false, secondInPairReduction of (x -> a, y -> inclusionOn(a)))(wellOrderTransitivity of p -> pair(a, inclusionOn(a)))
+        .withExplicitRules(secondInPairReduction of (x -> a, y -> inclusionOn(a)))(wellOrderTransitivity of p -> pair(a, inclusionOn(a)))
       thenHave(wellOrder(pair(a, inclusionOn(a))) |- forall(y, forall(z, (in(pair(c, y), inclusionOn(a)) /\ in(pair(y, z), inclusionOn(a))) ==> in(pair(c, z), inclusionOn(a))))) by InstantiateForall(
         c
       )
@@ -133,7 +133,7 @@ object Ordinals extends lisa.Main {
     thenHave((transitiveSet(a), wellOrder(pair(a, inclusionOn(a))), in(b, a)) |- (in(c, z) /\ in(z, b)) ==> in(c, b)) by Restate
     thenHave((transitiveSet(a), wellOrder(pair(a, inclusionOn(a))), in(b, a)) |- forall(z, (in(c, z) /\ in(z, b)) ==> in(c, b))) by RightForall
     thenHave((transitiveSet(a), wellOrder(pair(a, inclusionOn(a))), in(b, a)) |- forall(c, forall(z, (in(c, z) /\ in(z, b)) ==> in(c, b)))) by RightForall
-    thenHave((transitiveSet(a), wellOrder(pair(a, inclusionOn(a))), in(b, a)) |- transitiveSet(b)) by Substitution.apply2(true, transitiveSetInclusionDef of x -> b)
+    thenHave((transitiveSet(a), wellOrder(pair(a, inclusionOn(a))), in(b, a)) |- transitiveSet(b)) by Substitution.withExplicitRules(transitiveSetInclusionDef of x -> b)
     thenHave((transitiveSet(a), wellOrder(pair(a, inclusionOn(a)))) |- in(b, a) ==> transitiveSet(b)) by Restate
     thenHave((transitiveSet(a), wellOrder(pair(a, inclusionOn(a)))) |- forall(b, in(b, a) ==> transitiveSet(b))) by RightForall
 
@@ -192,8 +192,9 @@ object Ordinals extends lisa.Main {
           have(forall(z, (z === inclusionOrderOn(a)) <=> (z === pair(a, inclusionOn(a))))) by Weakening(inclusionOrderOn.definition)
           val incEq = thenHave(inclusionOrderOn(a) === pair(a, inclusionOn(a))) by InstantiateForall(inclusionOrderOn(a))
           have(total(secondInPair(inclusionOrderOn(a)), firstInPair(inclusionOrderOn(a)))) by Tautology.from(totalDef of p -> inclusionOrderOn(a), totA)
-          thenHave(total(secondInPair(pair(a, inclusionOn(a))), firstInPair(pair(a, inclusionOn(a))))) by Substitution.apply2(false, incEq)
-          val totIncA = thenHave(total(inclusionOn(a), a)) by Substitution.apply2(false, secondInPairReduction of (x -> a, y -> inclusionOn(a)), firstInPairReduction of (x -> a, y -> inclusionOn(a)))
+          thenHave(total(secondInPair(pair(a, inclusionOn(a))), firstInPair(pair(a, inclusionOn(a))))) by Substitution.withExplicitRules(incEq)
+          val totIncA =
+            thenHave(total(inclusionOn(a), a)) by Substitution.withExplicitRules(secondInPairReduction of (x -> a, y -> inclusionOn(a)), firstInPairReduction of (x -> a, y -> inclusionOn(a)))
 
           val totRelDef =
             have(total(r, x) <=> (relationBetween(r, x, x) /\ ∀(y, ∀(z, (in(y, x) /\ in(z, x)) ==> (in(pair(y, z), r) \/ in(pair(z, y), r) \/ (y === z)))))) by Weakening(total.definition)
@@ -235,11 +236,11 @@ object Ordinals extends lisa.Main {
         val incEq = thenHave(inclusionOrderOn(b) === pair(b, inclusionOn(b))) by InstantiateForall(inclusionOrderOn(b))
 
         have(secondInPair(pair(b, inclusionOn(b))) === inclusionOn(b)) by Weakening(secondInPairReduction of (x -> b, y -> inclusionOn(b)))
-        val snd = thenHave(secondInPair(inclusionOrderOn(b)) === inclusionOn(b)) by Substitution.apply2(true, incEq)
+        val snd = thenHave(secondInPair(inclusionOrderOn(b)) === inclusionOn(b)) by Substitution.withExplicitRules(incEq)
         have(firstInPair(pair(b, inclusionOn(b))) === (b)) by Weakening(firstInPairReduction of (x -> b, y -> inclusionOn(b)))
-        val fst = thenHave(firstInPair(inclusionOrderOn(b)) === (b)) by Substitution.apply2(true, incEq)
+        val fst = thenHave(firstInPair(inclusionOrderOn(b)) === (b)) by Substitution.withExplicitRules(incEq)
 
-        have(thesis) by Substitution.apply2(true, snd, fst)(totB)
+        have(thesis) by Substitution.withExplicitRules(snd, fst)(totB)
       }
 
       have(totalOrder(inclusionOrderOn(b)) <=> (partialOrder(inclusionOrderOn(b)) /\ total(secondInPair(inclusionOrderOn(b)), firstInPair(inclusionOrderOn(b))))) by Weakening(
@@ -275,9 +276,8 @@ object Ordinals extends lisa.Main {
             in(z, c) /\ forall(y, in(y, c) ==> (in(pair(z, y), secondInPair(pair(a, inclusionOn(a)))) \/ (z === y)))
           )
         )
-      ) by Substitution.apply2(false, incDef)
-      thenHave(forall(c, (subset(c, a) /\ !(c === emptySet())) ==> exists(z, in(z, c) /\ forall(y, in(y, c) ==> (in(pair(z, y), inclusionOn(a)) \/ (z === y)))))) by Substitution.apply2(
-        false,
+      ) by Substitution.withExplicitRules(incDef)
+      thenHave(forall(c, (subset(c, a) /\ !(c === emptySet())) ==> exists(z, in(z, c) /\ forall(y, in(y, c) ==> (in(pair(z, y), inclusionOn(a)) \/ (z === y)))))) by Substitution.withExplicitRules(
         firstInPairReduction of (x -> a, y -> inclusionOn(a)),
         secondInPairReduction of (x -> a, y -> inclusionOn(a))
       )
@@ -327,13 +327,13 @@ object Ordinals extends lisa.Main {
             in(z, c) /\ forall(y, in(y, c) ==> (in(pair(z, y), secondInPair(pair(b, inclusionOn(b)))) \/ (z === y)))
           )
         )
-      ) by Substitution.apply2(true, firstInPairReduction of (x -> b, y -> inclusionOn(b)), secondInPairReduction of (x -> b, y -> inclusionOn(b)))(woProp)
+      ) by Substitution.withExplicitRules(firstInPairReduction of (x -> b, y -> inclusionOn(b)), secondInPairReduction of (x -> b, y -> inclusionOn(b)))(woProp)
       thenHave(
         forall(
           c,
           (subset(c, firstInPair(inclusionOrderOn(b))) /\ !(c === emptySet())) ==> exists(z, in(z, c) /\ forall(y, in(y, c) ==> (in(pair(z, y), secondInPair(inclusionOrderOn(b))) \/ (z === y))))
         )
-      ) by Substitution.apply2(true, incDef)
+      ) by Substitution.withExplicitRules(incDef)
       have(thesis) by Tautology.from(lastStep, totalB, wellOrder.definition of p -> inclusionOrderOn(b))
     }
 

diff --git a/src/main/scala/lisa/mathematics/settheory/orderings/PartialOrders.scala b/src/main/scala/lisa/mathematics/settheory/orderings/PartialOrders.scala
@@ -273,7 +273,7 @@ object PartialOrders extends lisa.Main {
 
         val eqCase = have((y === t) |- (predecessor(p, t, x) \/ exists(y, in(pair(t, y), p2) /\ in(pair(y, x), p2)))) subproof {
           have(predecessor(p, y, x)) by Restate
-          thenHave((y === t) |- predecessor(p, t, x)) by Substitution.apply2(false, y === t)
+          thenHave((y === t) |- predecessor(p, t, x)) by Substitution.withExplicitRules(y === t)
           thenHave(thesis) by Weakening
         }