proposition: Lemma SBTM_HALT_enum : enumerable (SBTM_HALT).
proof: Proof. exists SBTM_HALT_enumerator. exact SBTM_HALT_enumerator_spec. Qed.
imports: Undecidability.TM.SBTM Undecidability.TM.Enumerators.SBTM_HALT_enum Undecidability.Synthetic.Definitions