proposition: Theorem fun_pos_finite_t_upto n : finite_t_upto (pos n -> X) (@fun_ext _ _).
proof: Proof. Proof using HX. assert (H : finite_t (vec X n)). { apply finite_t_vec; auto. } destruct H as (l & Hl). exists (map (@vec_pos _ _) l). intros f. exists (vec_pos (vec_set_pos f)); split. + apply in_map_iff; exists (vec_set_pos f); auto. + intros p; rew vec. Qed.
imports: List Arith Bool Eqdep_dec Undecidability.Synthetic.Definitions Undecidability.Synthetic.ReducibilityFacts Undecidability.Synthetic.InformativeDefinitions Undecidability.Synthetic.InformativeReducibilityFacts Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat finite) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.FOL.TRAKHTENBROT(notations utils fol_ops)