proposition: Lemma complement_SBTM_HALT_undec : undecidable (complement SBTM_HALT).
proof: Proof. intros H. eapply (dec_count_enum H), enumerator_enumerable. apply enumerator__T_sigT. - now apply (proj2_sig SBTM_HALT_enum.SBTM_enumeration). - intros M. now apply (proj2_sig (SBTM_HALT_enum.config_enumeration M)). Qed.
imports: Undecidability.Synthetic.Undecidability Undecidability.Synthetic(DecidabilityFacts EnumerabilityFacts) Undecidability.TM.SBTM