Weaken assumption of set_add lemmas to EqDecision (#355)

runtimeverification · Dec 8, 2023 · ee2e270 · ee2e270
1 parent 90fa9a6
commit ee2e270
Showing 1 changed file with 2 additions and 2 deletions.
diff --git 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.