diff --git a/theories/fin_sets.v b/theories/fin_sets.v
index 3c50fb3379361cbb366fa04e4aec383a9ca5f551..ed7e1034b49bd8598d64583744ec2386083242c5 100644
--- a/theories/fin_sets.v
+++ b/theories/fin_sets.v
@@ -475,10 +475,10 @@ Proof.
   - intros [X Hfin]. exists (elements X). set_solver.
 Qed.
 
-Lemma dec_pred_finite_set (P : A → Prop) `{!∀ x : A, Decision (P x)} :
+Lemma dec_pred_finite_set_alt (P : A → Prop) `{!∀ x : A, Decision (P x)} :
   pred_finite P ↔ (∃ X : C, ∀ x, P x ↔ x ∈ X).
 Proof.
-  rewrite dec_pred_finite; [|done]. split.
+  rewrite dec_pred_finite_alt; [|done]. split.
   - intros [xs Hfin]. exists (list_to_set xs). set_solver.
   - intros [X Hfin]. exists (elements X). set_solver.
 Qed.
diff --git a/theories/sets.v b/theories/sets.v
index 5651531fc79e51465e487a3baa1bf3bc0bc0138c..1f96052d995dd93f022083a206cf9a33ae9dfd06 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -1169,11 +1169,32 @@ Proof.
   intros xs. exists (fresh xs). split; [set_solver|]. apply infinite_is_fresh.
 Qed.
 
-Lemma dec_pred_finite {A} (P : A → Prop) `{!∀ x, Decision (P x)} :
+(** For decidable predicates, we have an alternative formulation for [pred_finite]. *)
+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.
-  split; intros [xs Hxs]; [|exists xs; set_solver].
-  exists (filter P xs). intros x. rewrite elem_of_list_filter. naive_solver.
+  split; intros [xs ?].
+  - exists (filter P xs). intros x. rewrite elem_of_list_filter. naive_solver.
+  - 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)} :