proposition: Fact pos_dec_rel2fun n (R : pos n -> pos n -> Prop) : (forall a b, { R a b } + { ~ R a b }) -> (forall p, ex (R p)) -> { f | forall p, R p (f p) }.
proof: Proof. apply finite_t_dec_choice; 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)