proposition: Lemma SBTM_HALT_undec : undecidable SBTM_HALT.
proof: Proof. intros H. now apply complement_SBTM_HALT_undec, dec_compl. Qed.
imports: Undecidability.Synthetic.Undecidability Undecidability.Synthetic(DecidabilityFacts EnumerabilityFacts) Undecidability.TM.SBTM