diff --git a/prelude/collections.v b/prelude/collections.v
index 9a08413fc54719d482aff268a4bf98c89174fee1..ef1103b26929d63719509d8e7084e958fd5d3755 100644
--- a/prelude/collections.v
+++ b/prelude/collections.v
@@ -115,15 +115,6 @@ Section simple_collection.
     Lemma non_empty_singleton_L x : {[ x ]} ≠ ∅.
     Proof. unfold_leibniz. apply non_empty_singleton. Qed.
   End leibniz.
-
-  Section dec.
-    Context `{∀ X Y : C, Decision (X ⊆ Y)}.
-    Global Instance elem_of_dec_slow (x : A) (X : C) : Decision (x ∈ X) | 100.
-    Proof.
-      refine (cast_if (decide_rel (⊆) {[ x ]} X));
-        by rewrite elem_of_subseteq_singleton.
-    Defined.
-  End dec.
 End simple_collection.
 
 (** * Tactics *)
diff --git a/prelude/fin_collections.v b/prelude/fin_collections.v
index 0fdf95e92131bd9d16cd70d3166cc890176152e7..fd557f5c0bdd7f14c748e4afc8cb2bbbf23ae3be 100644
--- a/prelude/fin_collections.v
+++ b/prelude/fin_collections.v
@@ -101,24 +101,12 @@ Proof.
     intros x; rewrite !elem_of_elements; set_solver.
   - intros. by rewrite elem_of_app, !elem_of_elements, elem_of_union.
 Qed.
+
 Instance elem_of_dec_slow (x : A) (X : C) : Decision (x ∈ X) | 100.
 Proof.
   refine (cast_if (decide_rel (∈) x (elements X)));
     by rewrite <-(elem_of_elements _).
 Defined.
-Global Program Instance collection_subseteq_dec_slow (X Y : C) :
-    Decision (X ⊆ Y) | 100 :=
-  match decide_rel (=) (size (X ∖ Y)) 0 return _ with
-  | left _ => left _ | right _ => right _
-  end.
-Next Obligation.
-  intros X Y E1 x ?; apply dec_stable; intro. destruct (proj1(elem_of_empty x)).
-  apply (size_empty_inv _ E1). by rewrite elem_of_difference.
-Qed.
-Next Obligation.
-  intros X Y E1 E2; destruct E1. apply size_empty_iff, equiv_empty. intros x.
-  rewrite elem_of_difference. intros [E3 ?]. by apply E2 in E3.
-Qed.
 Lemma size_union_alt X Y : size (X ∪ Y) = size X + size (Y ∖ X).
 Proof.
   rewrite <-size_union by set_solver.