proposition: Lemma mirrorConf_involution c : mirrorConf (mirrorConf c) = c.
proof: Proof. destruct c as [q t]. unfold mirrorConf. cbn. f_equal. apply mirror_tapes_involution. Qed.
imports: Undecidability(TM.Util.Prelim TM.Util.TM_facts)