proposition: Fact finite_discrete_choice : finite X -> (forall x, ex (R x)) -> exists f, forall x, R x (f x).
proof: Proof. Proof using X_discrete. intros (l & Hl) H. destruct list_discrete_choice with (l := l) as (f & Hf); auto. exists (fun x => f x (Hl x)); 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)