fact: Definition undecidable {X} (p : X -> Prop) := decidable p -> enumerable (complement SBTM_HALT).
imports: Undecidability.Synthetic.Definitions Undecidability.Synthetic.DecidabilityFacts Undecidability.Synthetic.ReducibilityFacts Undecidability.TM.SBTM