proposition: Lemma finite_sig_dec `{!EqDecision A} (P : A → Prop) `{Finite (sig P)} x : Decision (P x).
proof: 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.
imports: stdpp(options)