From ee2e27012dfd6721034f3ea887b40bc94d235b31 Mon Sep 17 00:00:00 2001
From: bmmoore <brandon.moore@runtimeverification.com>
Date: Fri, 8 Dec 2023 10:32:04 -0600
Subject: [PATCH] Weaken assumption of set_add lemmas to EqDecision (#355)

---
 theories/Lib/ListSetExtras.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/Lib/ListSetExtras.v b/theories/Lib/ListSetExtras.v
index 43bcdf45..a27e460a 100644
--- a/theories/Lib/ListSetExtras.v
+++ b/theories/Lib/ListSetExtras.v
@@ -262,7 +262,7 @@ Proof.
   by apply elem_of_cons in H0 as []; [| inversion H0].
 Qed.
 
-Lemma filter_set_add `{StrictlyComparable X} P
+Lemma filter_set_add `{EqDecision X} P
   `{forall (x : X), Decision (P x)} :
   forall (l : list X) x, ~ P x ->
   filter P l = filter P (set_add x l).
@@ -273,7 +273,7 @@ Proof.
     by destruct (decide (P hd)); rewrite <- IHl.
 Qed.
 
-Lemma set_add_ignore `{StrictlyComparable X} :
+Lemma set_add_ignore `{EqDecision X} :
   forall (l : list X) (x : X),
     x ∈ l ->
     set_add x l = l.