proposition: 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: Proof. split; intros [xs ?]. - exists (filter P xs). intros x. rewrite elem_of_list_filter. naive_solver. - exists xs. naive_solver. Qed.
imports: stdpp(finite) stdpp(options)