proposition: Fact fo_term_syms_map f t : fo_term_syms (fo_term_map f t) = fo_term_syms t.
proof: Proof. induction t as [ n | s v IHv ]; rew fot; auto; f_equal. do 2 rewrite flat_map_concat_map; f_equal. rewrite vec_list_vec_map, map_map. apply map_ext_in. intros x Hx; apply vec_list_inv in Hx. destruct Hx as (p & ->); apply IHv. Qed.
imports: List Arith Lia Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat finite) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.FOL.TRAKHTENBROT(notations utils decidable fol_ops fo_sig)