proposition: Lemma MoveToSymbol_skip t s : current t = Some s -> f s = false -> MoveToSymbol_Fun (doAct t (Some (g s), Rmove)) = MoveToSymbol_Fun t.
proof: Proof. intros H1 H2. cbn. symmetry. rewrite MoveToSymbol_Fun_equation. cbn. now rewrite H1, H2. 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)