fact: Record fo_simulation := Mk_fo_simulation { fos_simul :> X -> Y -> Prop; fos_syms : forall s v w, s ∊ ls -> (forall p, fos_simul (vec_pos v p) (vec_pos w p)) -> fos_simul (fom_syms M s v) (fom_syms N s w); fos_rels : forall r v w, r ∊ lr -> (forall p, fos_simul (vec_pos v p) (vec_pos w p)) -> fom_rels M r v <-> fom_rels N r w; fos_total : forall x, exists y, fos_simul x y; fos_surj : forall y, exists x, fos_simul x y; }.
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