proposition: Lemma midtape_right_rightof {Σ : finType} l m rs c n : n = 2 + (length rs) -> Nat.iter n (@tape_move_right Σ) (midtape l m (rs ++ [c])) = rightof c (rev rs ++ m :: l).
proof: Proof. intros ->. cbn. rewrite Nat_iter_S'. rewrite midtape_right_midtape; reflexivity. Qed.
imports: Undecidability.TM.Compound.TMTac Undecidability.TM.Basic.Mono Undecidability.TM.Compound.Multi Undecidability.TM.Combinators.Combinators Undecidability.TM.Compound.WriteString