proposition: Fact vec_reif X n (R : pos n -> X -> Prop) : (forall p, ex (R p)) -> exists v, forall p, R p (vec_pos v p).
proof: Proof. intros H. apply pos_reification in H. destruct H as (f & Hf). exists (vec_set_pos f). intro; rewrite vec_pos_set; trivial. 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)