proposition: Fact fo_term_subst_ext f g t : (forall x, In x (fo_term_vars t) -> f x = g x) -> t⟬f⟭ = t⟬g⟭.
proof: Proof. induction t as [ | s v IHv ]; intros Hfg; simpl. + apply Hfg; simpl; auto. + f_equal; apply vec_map_ext. intros x Hx. apply in_vec_list, vec_list_inv in Hx. destruct Hx as (p & ->). apply IHv. intros y Hy; apply Hfg. rewrite fo_term_vars_fix_1, in_flat_map. exists (vec_pos v p). split; auto; apply in_vec_list; 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)