proposition: Lemma MoveToSymbol_steps_mirror t : MoveToSymbol_L_steps t = MoveToSymbol_steps (mirror_tape t).
proof: Proof. functional induction MoveToSymbol_L_steps t; cbn; auto; simpl_tape in *; cbn in *; rewrite MoveToSymbol_steps_equation. - simpl_tape. now rewrite e, e0. - simpl_tape. rewrite e, e0. rewrite IHn. cbn. now simpl_tape. - simpl_tape. destruct (current t); cbn in *; easy. Qed.
imports: Undecidability(TM.Util.Prelim) Undecidability(TM.Basic.Mono) Undecidability(TM.Combinators.Combinators) Undecidability(TM.Compound.TMTac) Undecidability(TM.Compound.Multi) Coq(FunInd) Coq(Recdef)