proposition: Lemma finite_sig_pred_finite {A} (P : A → Prop) `{Finite (sig P)} : pred_finite P.
proof: Proof. exists (proj1_sig <$> enum _). intros x px. apply elem_of_list_fmap_1_alt with (x ↾ px); [apply elem_of_enum|]; done. Qed.
imports: stdpp(finite) stdpp(options)