proposition: Theorem list_discrete_choice l : (forall x, In x l -> ex (R x)) -> exists f, forall x (Hx : In x l), R x (f x Hx).
proof: Proof. Proof using X_discrete. induction l as [ | x l IHl ]; intros Hl. + exists (fun x (Hx : @In X x nil) => False_rect Y Hx). intros _ []. + destruct (Hl x) as (y & Hy); simpl; auto. destruct IHl as (f & Hf). * intros; apply Hl; simpl; auto. * assert (forall z, In z (x::l) -> x <> z -> In z l) as H1. { intros z [ -> | ] ?; tauto. } exists (fun z Hz => match X_discrete x z with | left _ => y | right H => f z (H1 _ Hz H) end). intros z Hz. destruct (X_discrete x z); subst; 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)