proposition: Theorem list_choose_dec ll : { l : _ & { x : _ & { r | ll = l++x::r /\ P x /\ forall y, In y l -> ~ P y } } } + { forall x, In x ll -> ~ P x }.
proof: Proof. Proof using Pdec. induction ll as [ | a ll IH ]; [ | destruct (Pdec a) as [ Ha | Ha ]; [ | destruct IH as [ (l & x & r & H1 & H2 & H3) | H ]] ]. * right; intros _ []. * left; exists nil, a, ll; repeat split; auto. * left; exists (a::l), x, r; repeat split; subst; auto. intros ? [ | ]; subst; auto. * right; intros ? [ | ]; subst; auto. Qed.
imports: List Arith Lia Permutation Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac)