diff --git a/theories/collections.v b/theories/collections.v
index 888be9b6503e9b41b8c2a83e5e4528febd2a0c6d..12ead0136104f5bfa5fe34e8d28be3ac4d1d373d 100644
--- a/theories/collections.v
+++ b/theories/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/theories/fin_collections.v b/theories/fin_collections.v
index 21d8476ab400143de205ceee1a43fb4de243a1a6..c4eb7c51c5813631d6f8273c0536fd54ba10542c 100644
--- a/theories/fin_collections.v
+++ b/theories/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.