proposition: Theorem constructive_choice X (T : X -> Type) (R : forall x, T x -> Prop) : (forall x, sig (R x)) -> { f : forall x, T x | forall x, R x (f x) }.
proof: Proof. intros f. exists (fun x => proj1_sig (f x)). intros x; apply (proj2_sig (f x)). 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)