proposition: Lemma doAct_mirror_multi (t : tapes sig n) (acts : Vector.t (option sig * move) n) : doAct_multi (mirror_tapes t) acts = mirror_tapes (doAct_multi t (mirror_acts acts)).
proof: Proof. apply Vector.eq_nth_iff; intros i ? <-. unfold doAct_multi, mirror_acts, mirror_tapes. simpl_tape. apply doAct_mirror. Qed.
imports: Undecidability(TM.Util.Prelim TM.Util.TM_facts)