proposition: Fact pos_reif_t X n (R : pos n -> X -> Prop) : (forall p, { x | R p x }) -> { f | forall p, R p (f p) }.
proof: Proof. apply constructive_choice. 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)