fact: Definition Mirror_trans : state (projT1 pM) * Vector.t (option sig) n -> state (projT1 pM) * Vector.t (option sig * move) n := fun qsym => let (q', act) := trans qsym in (q', mirror_acts act).
imports: Undecidability(TM.Util.Prelim TM.Util.TM_facts)