proposition: Lemma MoveToSymbol_mirror t t' : MoveToSymbol_Fun (mirror_tape t) = mirror_tape t' -> MoveToSymbol_L_Fun t = t'.
proof: Proof. functional induction MoveToSymbol_L_Fun t; intros H; cbn in *; try reflexivity; rewrite MoveToSymbol_Fun_equation in H; cbn; auto. - simpl_tape in *. rewrite e, e0 in H. cbn in *. simpl_tape in *. now apply mirror_tape_inv_midtape' in H as ->. - simpl_tape in *. rewrite e, e0 in H. cbn in *. simpl_tape in *. auto. - simpl_tape in *. destruct (current t); cbn in *; [easy|]. now apply mirror_tape_injective in H. 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)