proposition: Fact fot_def_map (f : nat -> nat) t : fot_definable t -> fot_definable (fun φ => t (fun n => φ (f n))).
proof: Proof. intros H; generalize (fot_def_ext H); revert H. intros (k & H1 & H2) H3. exists (fo_term_map f k); split. + rewrite fo_term_syms_map; auto. + intro phi; rewrite <- fo_term_subst_map; rew fot. rewrite H2; apply H3; intro; rew fot; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list finite) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.FOL.TRAKHTENBROT(notations utils fol_ops fo_sig fo_terms fo_logic)