proposition: Lemma current_chars_mirror_tapes (t : tapes sig n) : current_chars (mirror_tapes t) = current_chars t.
proof: Proof. apply Vector.eq_nth_iff; intros i ? <-. autounfold with tape. now simpl_tape. Qed.
imports: Undecidability(TM.Util.Prelim TM.Util.TM_facts)