proposition: Lemma mirror_step c : step (M := projT1 pM) (mirrorConf c) = mirrorConf (step (M := projT1 Mirror) c).
proof: Proof. unfold step; cbn -[doAct_multi]. unfold Mirror_trans. cbn. destruct c as [q t]; cbn. rewrite current_chars_mirror_tapes. destruct (trans (q, current_chars t)) as [q' acts]. unfold mirrorConf; cbn. f_equal. apply doAct_mirror_multi. Qed.
imports: Undecidability(TM.Util.Prelim TM.Util.TM_facts)