diff --git a/crates/formality-core/src/collections.rs b/crates/formality-core/src/collections.rs
index 84c5053e..63792ad3 100644
--- a/crates/formality-core/src/collections.rs
+++ b/crates/formality-core/src/collections.rs
@@ -70,13 +70,37 @@ impl<T: Ord + Clone> VecExt<T> for Vec<T> {
 }
 
 pub trait SetExt<T>: Sized {
-    fn split_first(self) -> Option<(T, Self)>;
+    fn split_first(self) -> Option<(T, Set<T>)>;
 
-    fn union_with(self, other: Self) -> Self;
+    fn union_with(self, other: impl Upcast<Set<T>>) -> Set<T>;
 
-    fn plus(self, other: T) -> Self;
+    fn with_element(self, other: impl Upcast<T>) -> Set<T>;
 
-    fn split_nth(&self, i: usize) -> Option<(T, Self)>;
+    fn without_element(self, other: impl Upcast<T>) -> Set<T>;
+
+    fn split_nth(&self, i: usize) -> Option<(T, Set<T>)>;
+}
+
+impl<T: Ord + Clone> SetExt<T> for &Set<T> {
+    fn split_first(self) -> Option<(T, Set<T>)> {
+        self.clone().split_first()
+    }
+
+    fn union_with(self, other: impl Upcast<Set<T>>) -> Set<T> {
+        self.clone().union_with(other)
+    }
+
+    fn with_element(self, other: impl Upcast<T>) -> Set<T> {
+        self.clone().with_element(other)
+    }
+
+    fn without_element(self, other: impl Upcast<T>) -> Set<T> {
+        self.clone().without_element(other)
+    }
+
+    fn split_nth(&self, i: usize) -> Option<(T, Set<T>)> {
+        <Set<T>>::split_nth(self, i)
+    }
 }
 
 impl<T: Ord + Clone> SetExt<T> for Set<T> {
@@ -87,22 +111,28 @@ impl<T: Ord + Clone> SetExt<T> for Set<T> {
         Some((e, c))
     }
 
-    fn split_nth(&self, i: usize) -> Option<(T, Self)> {
+    fn split_nth(&self, i: usize) -> Option<(T, Set<T>)> {
         let mut s = self.clone();
         let item = self.iter().skip(i).next()?;
         let item = s.take(item).unwrap();
         Some((item, s))
     }
 
-    fn union_with(mut self, other: Self) -> Self {
+    fn union_with(mut self, other: impl Upcast<Set<T>>) -> Set<T> {
+        let other: Set<T> = other.upcast();
         for item in other {
             self.insert(item);
         }
         self
     }
 
-    fn plus(mut self, other: T) -> Self {
-        self.insert(other);
+    fn with_element(mut self, other: impl Upcast<T>) -> Set<T> {
+        self.insert(other.upcast());
+        self
+    }
+
+    fn without_element(mut self, other: impl Upcast<T>) -> Set<T> {
+        self.remove(&other.upcast());
         self
     }
 }
diff --git a/crates/formality-core/src/judgment/proven_set.rs b/crates/formality-core/src/judgment/proven_set.rs
index 2d83d9c7..db5781d6 100644
--- a/crates/formality-core/src/judgment/proven_set.rs
+++ b/crates/formality-core/src/judgment/proven_set.rs
@@ -316,11 +316,12 @@ impl FailedJudgment {
                     // This will return a boolean indicating if all the failed rules
                     // ultimately failed because of a cycle.
 
+                    let mut stack1 = stack.clone();
+                    stack1.insert(&judgment.judgment);
+
                     let judgment_has_non_cycle;
-                    (judgment.failed_rules, judgment_has_non_cycle) = Self::strip_cycles(
-                        stack.clone().plus(&judgment.judgment),
-                        judgment.failed_rules,
-                    );
+                    (judgment.failed_rules, judgment_has_non_cycle) =
+                        Self::strip_cycles(stack1, judgment.failed_rules);
                     failed_rule.cause = RuleFailureCause::FailedJudgment(judgment);
 
                     if judgment_has_non_cycle.0 {