proposition: Lemma fin_destruct_O (i : Fin.t 0) : Empty_set.
proof: Proof. refine (match i with end). Qed.
imports: Undecidability.TM.Basic.Mono Undecidability.TM.Combinators.Combinators Undecidability.TM.Code.Code Undecidability.TM.Single.EncodeTapes Undecidability.TM.Compound(TMTac MoveToSymbol Multi Shift)