fact: Definition opt_to_sum_unit (X : Type) (x : option X) : X + unit := match x with | Some x => inl x | None => inr tt end.
imports: Undecidability.TM.Basic.Mono Undecidability.TM.Combinators.Combinators Undecidability.TM.Code.Code Undecidability.TM.Single.EncodeTapes Undecidability.TM.Compound(TMTac MoveToSymbol Multi Shift)