proposition: Lemma mirrorConf_injective c1 c2 : mirrorConf c1 = mirrorConf c2 -> c1 = c2.
proof: Proof. destruct c1 as [q1 t1], c2 as [q2 t2]. unfold mirrorConf. cbn. intros H; inv H. f_equal. now apply mirror_tapes_injective. Qed.
imports: Undecidability(TM.Util.Prelim TM.Util.TM_facts)