fact: Definition interp_s (d:D) : @interp Σ_funcs Σ_preds D := {| i_func := @i_func _ _ D I; i_atom := lift_s_semantically d |}.
imports: Undecidability.FOL.Syntax.Facts Undecidability.FOL.Syntax.Theories Undecidability.FOL.Semantics.Tarski.FragmentCore Undecidability(Shared.ListAutomation) Vector Lia