proposition: Theorem list_first_dec a ll : P a -> In a ll -> { l : _ & { x : _ & { r | ll = l++x::r /\ P x /\ forall y, In y l -> ~ P y } } }.
proof: Proof. Proof using Pdec. intros H1 H2. destruct (list_choose_dec ll) as [ H | H ]; trivial. destruct (H _ H2 H1). Qed.
imports: List Arith Lia Permutation Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac)