proposition: Lemma knowsFirstSymbols_nil {n : nat} (readSymbols : Vector.t (option sig) n) : knowsFirstSymbols readSymbols nil.
proof: Proof. destruct n. - revert readSymbols. apply Vector.case0. cbn. tauto. - rewrite (Vector.eta _). constructor. 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)