add some lemmas about `Finite` and `pred_finite`

Merge it if you like it. Feel free to suggest better naming and placement.

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.