proposition: Fact list_dec_choose_one l : (exists x, In x l /\ P x) -> { x | In x l /\ P x }.
proof: Proof. Proof using Pdec. clear HX Q HQ. induction l as [ | x l IHl ]; intros H. + exfalso; destruct H as (_ & [] & _). + destruct (Pdec x) as [ H1 | H1 ]. * exists x; simpl; auto. * destruct IHl as (y & H2 & H3). - destruct H as (y & [ -> | Hy ] & ?); firstorder. - exists y; simpl; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat fin_base) Undecidability.Shared.Libs.DLW.Vec(pos vec)