proposition: Fact fol_vars_subst σ (A : 𝔽) : fol_vars (A⦃σ⦄) = flat_map (fun x => fo_term_vars (σ x)) (fol_vars A).
proof: Proof. revert σ; induction A as [ | s r | b A HA B HB | q A HA ]; intros phi; auto. + simpl fol_vars. rewrite vec_list_vec_map. rewrite flat_map_flat_map. do 2 rewrite flat_map_concat_map. rewrite map_map; f_equal. apply map_ext; intros x. rewrite fo_term_vars_subst; auto. + simpl; rewrite flat_map_app; f_equal; auto. + simpl; rewrite HA. do 2 rewrite flat_map_flat_map. do 2 rewrite flat_map_concat_map; f_equal. apply map_ext_in; intros [ | x ] Hx; simpl; auto. rewrite fo_term_vars_map; rew fot. rewrite flat_map_concat_map, map_map. rewrite <- flat_map_concat_map. rewrite app_nil_r. rewrite flat_map_single, map_id; auto. Qed.
imports: List Arith Lia 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 fo_sig fo_terms) Undecidability.Shared.ListAutomation