fact: Definition FSAT (phi : form) := exists D (I : interp D) rho, listable D /\ (forall p, decidable (fun v => i_atom (P:=p) v)) /\ rho ⊨ phi.
imports: Undecidability.FOL.Semantics(Tarski.FragmentFacts) Undecidability.FOL.Syntax(Facts) Undecidability.Synthetic.DecidabilityFacts Undecidability.Shared.Dec List