proposition: Lemma direction_enumeration : { e | enumerator__T e direction}.
proof: Proof. exists (fun n => match n with 0 => Some go_left | _ => Some go_right end). now intros []; [exists 0|exists 1]. Qed.
imports: Undecidability.Synthetic(Definitions EnumerabilityFacts) Undecidability.TM.SBTM