fact: Definition exploding D (M : interp D) (F_P:Prop) := forall rho phi, sat_bot F_P rho (⊥ → phi).
imports: Undecidability.FOL.Syntax.Facts Undecidability.FOL.Syntax.Theories Undecidability.FOL.Semantics.Tarski.FragmentCore Undecidability(Shared.ListAutomation) Vector Lia