diff --git a/theories/finite.v b/theories/finite.v
index 0cd64c40c3f9dea81fa091d4752503bfc2ce19bd..9bde7e8770b4f730dc987b04f0ae523a464a4555 100644
--- a/theories/finite.v
+++ b/theories/finite.v
@@ -377,18 +377,11 @@ Proof. unfold card; simpl. induction n; simpl; rewrite ?fmap_length; auto. Qed.
 Lemma finite_sig_dec `{!EqDecision A} (P : A → Prop) `{Finite (sig P)} x :
   Decision (P x).
 Proof.
-  assert (∀ px, (x ↾ px) ∈ enum (sig P)) as Helems by auto using elem_of_enum.
-  assert (Decision {px | (x ↾ px) ∈ enum (sig P)}) as [[px ?]|Hno_px].
-  { induction (enum _) as [ | [y py] elems IH].
-    { right. by intros [? ?%not_elem_of_nil]. }
-    destruct (decide (x = y)) as [-> | ?].
-    { left. exists py. by left. }
-    destruct IH as [[px ?]|?].
-    { intros px. specialize (Helems px) as ?%elem_of_cons. naive_solver. }
-    - left. by exists px.
-    - right. intros [px ?%elem_of_cons]. naive_solver. }
-  - by left.
-  - right. intros px. apply Hno_px. by exists px.
+  assert {xs : list A | ∀ x, P x ↔ x ∈ xs} as [xs ?].
+  { clear x. exists (proj1_sig <$> enum _). intros x. split; intros Hx.
+    - apply elem_of_list_fmap_1_alt with (x ↾ Hx); [apply elem_of_enum|]; done.
+    - apply elem_of_list_fmap in Hx as [[x' Hx'] [-> _]]; done. }
+  destruct (decide (x ∈ xs)); [left | right]; naive_solver.
 Qed.
 
 Section sig_finite.
diff --git a/theories/sets.v b/theories/sets.v
index 1f96052d995dd93f022083a206cf9a33ae9dfd06..6152085c67f807e3e25f05a3ea7ae89012c5ac17 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -1169,7 +1169,8 @@ Proof.
   intros xs. exists (fresh xs). split; [set_solver|]. apply infinite_is_fresh.
 Qed.
 
-(** For decidable predicates, we have an alternative formulation for [pred_finite]. *)
+(** This formulation of finiteness is stronger than [pred_finite]: when equality
+    is decidable, it is equivalent to the predicate being finite AND decidable. *)
 Lemma dec_pred_finite_alt {A} (P : A → Prop) `{!∀ x, Decision (P x)} :
   pred_finite P ↔ ∃ xs : list A, ∀ x, P x ↔ x ∈ xs.
 Proof.
@@ -1178,25 +1179,6 @@ Proof.
   - exists xs. naive_solver.
 Qed.
 
-(** Conversely (if equality is decidable), the alternative formulation makes the
-    predicate decidable; so it is stronger than [pred_finite] (there are finite
-    which are undecidable, for instance [λ (), Q] where [Q] is undecidable). *)
-Lemma pred_finite_alt_dec {A} `{!EqDecision A} (P : A → Prop) :
-  {xs : list A | ∀ x, P x ↔ x ∈ xs} → pred_finite P * (∀ x, Decision (P x)).
-Proof.
-  intros [xs ?]. split.
-  - exists xs. naive_solver.
-  - intros x. destruct (decide (x ∈ xs)); [left | right]; naive_solver.
-Qed.
-
-Lemma finite_sig_pred_finite_alt {A} (P : A → Prop) `{Finite (sig P)} :
-  {xs : list A | ∀ x, P x ↔ x ∈ xs}.
-Proof.
-  exists (proj1_sig <$> enum _). intros x. split.
-  - intros px. apply elem_of_list_fmap_1_alt with (x ↾ px); [apply elem_of_enum|]; done.
-  - intros Hx. apply elem_of_list_fmap in Hx as [[x' px'] [-> _]]. done.
-Qed.
-
 Lemma finite_sig_pred_finite {A} (P : A → Prop) `{Finite (sig P)} :
   pred_finite P.
 Proof.