proposition: Fact fo_term_vars_subst f t : fo_term_vars (t⟬f⟭) = flat_map (fun n => fo_term_vars (f n)) (fo_term_vars t).
proof: Proof. induction t as [ n | s v IHv ]; rew fot; auto. + simpl; rewrite app_nil_r; auto. + rewrite vec_list_vec_map. rewrite flat_map_flat_map. rewrite flat_map_concat_map, map_map, <- flat_map_concat_map. do 2 rewrite flat_map_concat_map; f_equal. apply map_ext_in; intros x Hx. apply vec_list_inv in Hx. destruct Hx as (p & ->). rewrite IHv; auto. 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)