fact: Definition fo_form_fin_dec_SAT_in X := exists (M : fo_model Σ X) (_ : finite_t X) (_ : fo_model_dec M) (φ : nat -> X), fol_sem M φ A.
imports: List Undecidability.Shared.Libs.DLW.Utils(finite) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.FOL.TRAKHTENBROT(notations utils decidable fol_ops fo_sig fo_terms fo_logic)