proposition: Fact fo_term_sem_ext t φ ψ : (forall n, In n (fo_term_vars t) -> φ n = ψ n) -> ⟦t⟧ φ = ⟦t⟧ ψ.
proof: Proof. induction t as [ n | s v IHv ] in φ, ψ |- *; intros H; rew fot. + apply H; 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; auto. intros n Hn; apply H; rew fot. apply 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)