proposition: Theorem btm_ex_dec t : (forall x, x ∈ t -> { P x } + { ~ P x }) -> { s | s ∈ t /\ P s } + { forall s, s ∈ t -> ~ P s }.
proof: Proof. Proof using HP. intros H. destruct (btm_finite_t t) as (l & Hl). destruct list_choose_dep with (P := P) (Q := fun x => ~ P x) (l := l) as [ (s & H1 & H2) | H1 ]. + intros; apply H, Hl; eauto. + left; exists s; split; auto; apply Hl; eauto. + right; intros s H2 H3. apply Hl in H2 as (s' & H2 & H4). apply (H1 _ H4); eauto. Qed.
imports: List Arith Lia Max Wellfounded Setoid Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_decidable finite seteq) Undecidability.Shared.Libs.DLW.Vec(pos) Undecidability.Shared.Libs.DLW.Wf(wf_finite wf_chains) Undecidability.FOL.TRAKHTENBROT(notations fol_ops)