proposition: Lemma knowsFirstSymbols_all' n (T : tapes sig n) (symbols : Vector.t (option sig) n) : knowsFirstSymbols symbols (vector_to_list T) -> symbols = current_chars T.
proof: Proof. induction T as [ | tp n T IH]; intros; cbn in *. - clear H. revert symbols. apply Vector.case0. reflexivity. - rewrite (Vector.eta symbols) in *. unfold current_chars. cbn in *. destruct H as [ <- H]. f_equal. auto. 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)