proposition: Corollary MoveToSymbol_L_correct_midtape ls ls' rs m x : stop m = false -> (forall x, List.In x ls -> stop x = false) -> stop x = true -> MoveToSymbol_L_Fun stop f (midtape (ls ++ x :: ls') m rs) = midtape ls' (f x) (rev (map f ls) ++ (f m) :: rs).
proof: Proof. intros HStopM HStopRs HStopX. unshelve epose proof (@MoveToSymbol_L_correct (midtape (ls ++ x :: ls') m rs) (m::ls) ls' x _ HStopX eq_refl) as Lmove. { intros ? [->|?]; auto. } cbn in *. now rewrite <- app_assoc in Lmove. 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)