fact: Definition fol_definable (R : (nat -> X) -> Prop) := { A | incl (fol_syms A) ls /\ incl (fol_rels A) lr /\ forall φ, fol_sem M φ A <-> R φ }.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list finite) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.FOL.TRAKHTENBROT(notations utils fol_ops fo_sig fo_terms fo_logic)