proposition: Corollary MoveToSymbol_correct_midtape ls rs rs' m x : stop m = false -> (forall x, List.In x rs -> stop x = false) -> stop x = true -> MoveToSymbol_Fun stop f (midtape ls m (rs ++ x :: rs')) = midtape (rev (map f rs) ++ (f m) :: ls) (f x) rs'.
proof: Proof. intros HStopM HStopRs HStopX. unshelve epose proof (@MoveToSymbol_correct (midtape ls m (rs ++ x :: rs')) (m::rs) rs' 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)