proposition: Lemma MoveToSymbol_Step_Fun_M2_true t x : current t = Some x -> f x = true -> MoveToSymbol_Fun t = MoveToSymbol_Step_Fun t.
proof: Proof. intros H1 H2. destruct t; cbn in *; inv H1. rewrite MoveToSymbol_Fun_equation, H2. cbn. now rewrite 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)