When removing a formula from a sequent, remove all isSame formulas

Created by: cache-nez

When removing a formula from the set, representing the left or the right side of a sequent, it is easy to attempt removing an equivalent formula instead of the exact one, contained in the set. This PR first attempts to remove the exact formula from the sequent, and if such is not found, filters out all isSame formulas.

This increases the runtime of the removal from O(1) to O(n)!

However, it is hard to ensure that the removal is always performed on the exact formula that's contained in the sequent. We can come back to this question later, when we start investigating performance.

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))
   }
 
   /**