proposition: Lemma Mirror_Realise R : pM ⊨ R -> Mirror ⊨ Mirror_Rel R.
proof: Proof. intros HRealise. intros t i outc HLoop. apply (HRealise (mirror_tapes t) i (mirrorConf outc)). now apply mirror_lift in HLoop. Qed.
imports: Undecidability(TM.Util.Prelim TM.Util.TM_facts)