fact: Fixpoint impl {Σ_funcs : funcs_signature} {Σ_preds : preds_signature} {ff : falsity_flag} (A : list form) phi := match A with | [] => phi | psi :: A => bin _ _ full_operators _ Impl psi (impl A phi) end.
imports: Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability(Shared.ListAutomation) Undecidability(Shared.Libs.PSL.Vectors.Vectors)