fact: Definition sat_bot {ff : falsity_flag} (F_P : Prop) (rho : env D) (phi : form) : Prop := @sat _ Σ_preds_bot D (interp_bot F_P I) falsity_off rho (falsity_to_pred phi).
imports: Undecidability.FOL.Syntax.Facts Undecidability.FOL.Syntax.Theories Undecidability.FOL.Semantics.Tarski.FragmentCore Undecidability(Shared.ListAutomation) Vector Lia