proposition: Lemma doAct_nop tapes : doAct_multi tapes nop_action = tapes.
proof: Proof. unfold nop_action, doAct_multi. apply Vector.eq_nth_iff; intros ? i <-. erewrite Vector.nth_map2; eauto. rewrite Vector.const_nth. cbn. reflexivity. Qed.
imports: Undecidability.Shared.Libs.PSL.Vectors.Vectors Undecidability.TM.TM