diff --git a/lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala b/lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala
index e372a02e2bba7521a30d19f3ed6117872053289c..94f5fb0edba8201ecd22e6227f0520b6451979aa 100644
--- a/lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala
@@ -98,17 +98,21 @@ trait KernelHelpers {
 
   val emptySeq: Sequent = Sequent(Set.empty, Set.empty)
 
+  private def removeFormula(s: Set[Formula], f: Formula): Set[Formula] = {
+    if (s.contains(f)) s - f else s.filterNot(isSame(_, f))
+  }
+
   extension (s: Sequent) {
     infix def +<(f: Formula): Sequent = s.copy(left = s.left + f)
-    infix def -<(f: Formula): Sequent = s.copy(left = s.left - f)
+    infix def -<(f: Formula): Sequent = s.copy(left = removeFormula(s.left, f))
     infix def +>(f: Formula): Sequent = s.copy(right = s.right + f)
-    infix def ->(f: Formula): Sequent = s.copy(right = s.right - f)
+    infix def ->(f: Formula): Sequent = s.copy(right = removeFormula(s.right, f))
     infix def ++<(s1: Sequent): Sequent = s.copy(left = s.left ++ s1.left)
-    infix def --<(s1: Sequent): Sequent = s.copy(left = s.left -- s1.left)
+    infix def --<(s1: Sequent): Sequent = s.copy(left = s1.left.foldLeft(s.left)(removeFormula))
     infix def ++>(s1: Sequent): Sequent = s.copy(right = s.right ++ s1.right)
-    infix def -->(s1: Sequent): Sequent = s.copy(right = s.right -- s1.right)
+    infix def -->(s1: Sequent): Sequent = s.copy(right = s1.right.foldLeft(s.right)(removeFormula))
     infix def ++(s1: Sequent): Sequent = s.copy(left = s.left ++ s1.left, right = s.right ++ s1.right)
-    infix def --(s1: Sequent): Sequent = s.copy(left = s.left -- s1.left, right = s.right -- s1.right)
+    infix def --(s1: Sequent): Sequent = s.copy(left = s1.left.foldLeft(s.left)(removeFormula), right = s1.right.foldLeft(s.right)(removeFormula))
   }
 
   /**
diff --git a/lisa-utils/src/test/scala/lisa/utils/SequentUtilsTest.scala b/lisa-utils/src/test/scala/lisa/utils/SequentUtilsTest.scala
new file mode 100644
index 0000000000000000000000000000000000000000..846b131b51a74e7db60483e22f04719a97c0f5b9
--- /dev/null
+++ b/lisa-utils/src/test/scala/lisa/utils/SequentUtilsTest.scala
@@ -0,0 +1,56 @@
+package lisa.utils
+
+import lisa.kernel.fol.FOL.*
+import lisa.kernel.proof.SequentCalculus.Sequent
+import lisa.kernel.proof.SequentCalculus.isSameSequent
+import lisa.test.ProofCheckerSuite
+import lisa.utils.Helpers.*
+
+import scala.collection.immutable.Set
+
+class SequentUtilsTest extends ProofCheckerSuite {
+  val simpleSequent: Sequent = s === t |- s === t
+  val sequent: Sequent = Set(s === t, t === u) |- Set(s === t, s === u)
+  val emptySequent: Sequent = () |- ()
+
+  test("left remove formula") {
+    val leftFormula = simpleSequent.left.head
+    // plain removal
+    assert((simpleSequent -< leftFormula) === (() |- simpleSequent.right))
+    // isSame removal
+    val sameFormula = leftFormula /\ (s === s)
+    assert(!(sameFormula == leftFormula))
+    assert(isSame(leftFormula, sameFormula))
+    assert((simpleSequent -< sameFormula) === (simpleSequent -< leftFormula))
+  }
+
+  test("right remove formula") {
+    val rightFormula = simpleSequent.right.head
+    // plain removal
+    assert((simpleSequent -> rightFormula) === (simpleSequent.left |- ()))
+    // isSame removal
+    val sameFormula = rightFormula /\ (s === s)
+    assert(!(sameFormula == rightFormula))
+    assert(isSame(rightFormula, sameFormula))
+    assert((simpleSequent -> sameFormula) === (simpleSequent -> rightFormula))
+  }
+
+  test("left remove set") {
+    assert(sequent --< sequent === (() |- sequent.right))
+    val sameLeft = Sequent(sequent.left.map(_ /\ (u === u)), sequent.right)
+    assert((sequent --< sameLeft) === (() |- sequent.right))
+  }
+
+  test("right remove set") {
+    assert((sequent --> sequent) === (sequent.left |- ()))
+    val sameRight = Sequent(sequent.left, sequent.right.map(_ /\ (u === u)))
+    assert(!(sequent.right === sameRight))
+    assert(isSameSet(sequent.right, sameRight.right))
+    assert(sequent --> sameRight === (sequent.left |- ()))
+  }
+
+  test("sequent remove sequent") {
+    val equivalentSequent = Set((s === t) /\ (s === s), t === u) |- Set(s === t, (s === u) /\ (u === u))
+    assert(sequent -- equivalentSequent === emptySequent)
+  }
+}