proposition: Theorem finite_t_find_dec X (P : X -> Prop) (Pdec : forall x, { P x } + { ~ P x }) (HQ : finite_t X) : { x | P x } + { forall x, ~ P x }.
proof: Proof. destruct HQ as (l & Hl). destruct list_choose_dep with (P := P) (Q := fun x => ~ P x) (l := l) as [ (? & ? & ?) | ]; eauto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_decidable fin_base)