proposition: Theorem fun_finite_t_upto : finite_t_upto (X -> Y) (@fun_ext _ _).
proof: Proof. Proof using HY HX2 HX1. destruct finite_t_discrete_bij_t_pos with X as (n & i & j & Hji & Hij); auto. destruct fun_pos_finite_t_upto with Y n as (l & Hl); auto. exists (map (fun f x => f (i x)) l). intros f. destruct (Hl (fun p => f (j p))) as (g & H1 & H2). exists (fun x => g (i x)); split. + apply in_map_iff; exists g; auto. + intros x. red in H2. rewrite <- (Hji x) at 1; auto. 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)