diff --git a/lisa-kernel/src/main/scala/lisa/kernel/fol/EquivalenceChecker.scala b/lisa-kernel/src/main/scala/lisa/kernel/fol/EquivalenceChecker.scala
index 70bb9a286ae38fe429eee8d2fa998a528bcb969b..adfeb547170d2d18e7a8f003c1c1fced7a313631 100644
--- a/lisa-kernel/src/main/scala/lisa/kernel/fol/EquivalenceChecker.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/fol/EquivalenceChecker.scala
@@ -108,12 +108,6 @@ private[fol] trait EquivalenceChecker extends FormulaDefinitions {
       if (value) lessThanBitSet.update(otherIx + 1, true)
     }
 
-    // TODO: Check if needed
-    override def equals(obj: Any): Boolean = obj match {
-      case f: NormalFormula => eq(f)
-      case _ => super.equals(obj)
-    }
-
     def recoverFormula: Formula = toFormulaAIG(this)
   }
   sealed abstract class NonTraversable extends NormalFormula
@@ -400,7 +394,7 @@ private[fol] trait EquivalenceChecker extends FormulaDefinitions {
             case (NormalSchemConnector(id1, args1, polarity1), NormalSchemConnector(id2, args2, polarity2)) =>
               id1 == id2 && polarity1 == polarity2 && args1.zip(args2).forall(f => latticesEQ(f._1, f._2))
             case (NormalForall(x1, inner1, polarity1), NormalForall(x2, inner2, polarity2)) =>
-              polarity1 == polarity2 && latticesLEQ(inner1, inner2)
+              polarity1 == polarity2 && (if (polarity1) latticesLEQ(inner1, inner2) else latticesLEQ(inner2, inner1))
             case (_: NonTraversable, _: NonTraversable) => false
 
             case (_, NormalAnd(children, true)) =>
diff --git a/src/main/scala/lisa/mathematics/SetTheory.scala b/src/main/scala/lisa/mathematics/SetTheory.scala
index 7f301e919e4832a97120c74702d295a703697840..fc33f2dd4cf3bfe6dfb38d8b90e799d4b5d98479 100644
--- a/src/main/scala/lisa/mathematics/SetTheory.scala
+++ b/src/main/scala/lisa/mathematics/SetTheory.scala
@@ -868,7 +868,7 @@ object SetTheory extends lisa.Main {
       val exRed = thenHave(exists(b, in(b, x) /\ in(t, b)) |- exists(b, in(b, x))) by LeftExists
 
       have(in(t, union(x)) |- exists(b, in(b, x))) by Cut(unionAx, exRed)
-      thenHave(thesis) by Weakening
+      thenHave(thesis) by Tautology
     }
 
     val rhs = have(∀(b, in(b, x) ==> in(t, b)) /\ exists(b, in(b, x)) |- (in(t, union(x)) /\ ∀(b, in(b, x) ==> in(t, b)))) subproof {