proposition: Lemma SBTM_HALT_INSTANCE_enumeration : { e | enumerator__T e {M : SBTM & config M }}.
proof: Proof. eexists. apply enumerator__T_sigT. - apply (proj2_sig SBTM_enumeration). - intros M. apply (proj2_sig (config_enumeration M)). Qed.
imports: Undecidability.Synthetic(Definitions EnumerabilityFacts) Undecidability.TM.SBTM