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..d15bfcfb8571c6d2cfe7d41759e509fa60edf33d 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 (P : A → Prop) {Hdec : ∀ x : A, Decision (P x)} :
+  pred_finite P ↔ (∃ X : C, ∀ x, P x ↔ x ∈ X).
+Proof.
+  rewrite dec_pred_finite; [|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..6436fae23ad629b495c071701344c0f4fbd34561 100644
--- a/theories/finite.v
+++ b/theories/finite.v
@@ -373,6 +373,34 @@ Qed.
 Lemma fin_card n : card (fin n) = n.
 Proof. unfold card; simpl. induction n; simpl; rewrite ?fmap_length; auto. Qed.
 
+Lemma finite_dec (P : Prop) `{Hfin : Finite P} : Decision P.
+Proof.
+  destruct Hfin as [[ | p proofs'] _ Hproofs].
+  { right. intros p. specialize (Hproofs p) as ?%not_elem_of_nil. naive_solver. }
+  { left. done. }
+Qed.
+
+(* shouldn’t be an instance (cycle with [sig_finite]): *)
+Lemma finite_sig_dec {A} {Heqdec : EqDecision A} (P : A → Prop) `{Hfin : Finite (sig P)} :
+  ∀ x, Decision (P x).
+Proof.
+  intros x. destruct Hfin as [elems _ Helems'].
+  assert (∀ px, (x ↾ px) ∈ elems) as Helems by done; clear Helems'.
+  assert (Decision {px | (x ↾ px) ∈ elems}) as [[px ?] | no_px].
+  {
+    induction elems as [ | [y py] elems' IH].
+    { right. intros [? ?%not_elem_of_nil]. naive_solver. }
+    { destruct (decide (x = y)) as [-> | ?].
+      { left. by exists py. }
+      { destruct IH as [[px ?] | no_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 no_px. by exists px. }
+Qed.
+
 Section sig_finite.
   Context {A} (P : A → Prop) `{∀ x, Decision (P x)}.
 
diff --git a/theories/sets.v b/theories/sets.v
index 6ac9a22e5db68e16d6b63d5f17b677b780bf26c8..27925908936cedc30c3b28a1f565997bbafef58f 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -1169,6 +1169,46 @@ Proof.
   intros xs. exists (fresh xs). split; [set_solver|]. apply infinite_is_fresh.
 Qed.
 
+Lemma dec_pred_finite {A} (P : A → Prop) {Hdec : ∀ x, Decision (P x)} :
+  pred_finite P ↔ ∃ (xs : list A), ∀ x, P x ↔ x ∈ xs.
+Proof.
+  split; intros [xs Hxs]; [|exists xs; set_solver].
+  cut (∀ n, ∃ ys, (∀ x, P x → x ∈ ys ++ drop n xs) ∧ (∀ x, x ∈ ys → P x)).
+  { intros H. specialize (H (length xs)) as (ys & H1 & H2).
+    rewrite drop_all, app_nil_r in H1. exists ys. set_solver. }
+  intros n. induction n as [ | n (ys & IH1 & IH2)].
+  { exists []. rewrite drop_0. set_solver. }
+  destruct (decide (n < length xs)) as [[y Hn]%lookup_lt_is_Some | ?].
+  { destruct (decide (P y)) as [Hy | Hy].
+    { exists (ys ++ [y]). pose proof (assoc app) as <-. cbn.
+      rewrite <-drop_S; set_solver. }
+    { exists ys. split; [|done]. intros x Hx.
+      specialize (IH1 x Hx) as [? | Hx_elem_of]%elem_of_app; [set_solver|].
+      erewrite drop_S in Hx_elem_of; set_solver. } }
+  { exists ys. revert IH1. rewrite !drop_ge, app_nil_r; [done|lia..]. }
+Qed.
+
+Lemma finite_sig_pred_finite {A} (P : A → Prop) `{Hfin : 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) :
+  pred_finite (uncurry P) → ∀ x, pred_finite (P x).
+Proof.
+  intros [xys ?] x. 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) :
+  pred_finite (uncurry P) → ∀ y, pred_finite (flip P y).
+Proof.
+  intros [xys ?] y. 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)]. *)