diff --git a/CHANGELOG.md b/CHANGELOG.md
index 2a65cfe9e979d1ee78562e3c1dfd4b8e83a47b61..08921ad35e67a23e789457698ce21c7f38c44995 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -15,6 +15,7 @@ Coq 8.10 is no longer supported by this release.
 - Rename `decide_iff` → `decide_ext` and `bool_decide_iff` → `bool_decide_ext`.
 - Remove a spurious `Global Arguments Pos.of_nat : simpl never`.
 - Add tactics `destruct select <pat>` and `destruct select <pat> as <intro_pat>`.
+- Add some more lemmas about `Finite` and `pred_finite`.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
diff --git a/theories/fin_sets.v b/theories/fin_sets.v
index e9afdfb072349834054573494c2a39d0065977f9..ed7e1034b49bd8598d64583744ec2386083242c5 100644
--- a/theories/fin_sets.v
+++ b/theories/fin_sets.v
@@ -475,6 +475,14 @@ Proof.
   - intros [X Hfin]. exists (elements X). set_solver.
 Qed.
 
+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_alt; [|done]. split.
+  - intros [xs Hfin]. exists (list_to_set xs). set_solver.
+  - intros [X Hfin]. exists (elements X). set_solver.
+Qed.
+
 Lemma pred_infinite_set (P : A → Prop) :
   pred_infinite P ↔ (∀ X : C, ∃ x, P x ∧ x ∉ X).
 Proof.
diff --git a/theories/finite.v b/theories/finite.v
index 8ec114313a2f979ee97d250791ccaed48ae37a37..b2fa877ec8c197ec723e734a3823c8bb8e9d7b4c 100644
--- a/theories/finite.v
+++ b/theories/finite.v
@@ -373,6 +373,17 @@ Qed.
 Lemma fin_card n : card (fin n) = n.
 Proof. unfold card; simpl. induction n; simpl; rewrite ?fmap_length; auto. Qed.
 
+(* shouldn’t be an instance (cycle with [sig_finite]): *)
+Lemma finite_sig_dec `{!EqDecision A} (P : A → Prop) `{Finite (sig P)} x :
+  Decision (P x).
+Proof.
+  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. (* <- could be Defined but this lemma will probably not be used for computing *)
+
 Section sig_finite.
   Context {A} (P : A → Prop) `{∀ x, Decision (P x)}.
 
diff --git a/theories/sets.v b/theories/sets.v
index 6ac9a22e5db68e16d6b63d5f17b677b780bf26c8..6152085c67f807e3e25f05a3ea7ae89012c5ac17 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -1169,6 +1169,37 @@ Proof.
   intros xs. exists (fresh xs). split; [set_solver|]. apply infinite_is_fresh.
 Qed.
 
+(** 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.
+  split; intros [xs ?].
+  - exists (filter P xs). intros x. rewrite elem_of_list_filter. naive_solver.
+  - exists xs. naive_solver.
+Qed.
+
+Lemma finite_sig_pred_finite {A} (P : A → Prop) `{Finite (sig P)} :
+  pred_finite P.
+Proof.
+  exists (proj1_sig <$> enum _). intros x px.
+  apply elem_of_list_fmap_1_alt with (x ↾ px); [apply elem_of_enum|]; done.
+Qed.
+
+Lemma pred_finite_arg2 {A B} (P : A → B → Prop) x :
+  pred_finite (uncurry P) → pred_finite (P x).
+Proof.
+  intros [xys ?]. exists (xys.*2). intros y ?.
+  apply elem_of_list_fmap_1_alt with (x, y); by auto.
+Qed.
+
+Lemma pred_finite_arg1 {A B} (P : A → B → Prop) y :
+  pred_finite (uncurry P) → pred_finite (flip P y).
+Proof.
+  intros [xys ?]. exists (xys.*1). intros x ?.
+  apply elem_of_list_fmap_1_alt with (x, y); by auto.
+Qed.
+
 (** Sets of sequences of natural numbers *)
 (* The set [seq_seq start len] of natural numbers contains the sequence
 [start, start + 1, ..., start + (len-1)]. *)