proposition: Lemma tapeToList_move (t : tape) (D : move) : tapeToList (tape_move t D) = tapeToList t.
proof: Proof. destruct t, D; cbn; auto. - revert s l0. induction l; intros; cbn in *; simpl_list; auto. - revert s l. induction l0; intros; cbn in *; simpl_list; auto. Qed.
imports: Undecidability.Shared.Libs.PSL.Vectors.Vectors Undecidability.TM.TM