proposition: Lemma doAct_mirror (t : tape sig) (act : option sig * move) : doAct (mirror_tape t) act = mirror_tape (doAct t (mirror_act act)).
proof: Proof. now destruct act as [ [ s | ] [ | | ]]; cbn; simpl_tape. Qed.
imports: Undecidability(TM.Util.Prelim TM.Util.TM_facts)