proposition: Lemma SBTM_HALT_enumerator_spec : enumerator SBTM_HALT_enumerator SBTM_HALT.
proof: Proof. exact (proj2_sig SBTM_HALT_enumeration). Qed.
imports: Undecidability.Synthetic(Definitions EnumerabilityFacts) Undecidability.TM.SBTM