fact: Definition fot_vec_env Σ n p : { w : vec (fo_term (ar_syms Σ)) n | (forall X (M : fo_model Σ X) v φ q x, fo_term_sem M x·(env_vlift φ v) (vec_pos w q) = vec_pos (vec_change v p x) q) /\ forall q, fo_term_syms (vec_pos w q) = nil }.
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