proposition: Lemma mirror_unlift k c1 c2 : loopM (M := projT1 pM) (mirrorConf c1) k = Some (mirrorConf c2) -> loopM (M := projT1 Mirror) ( c1) k = Some ( c2).
proof: Proof. unfold loopM. intros HLoop. apply loop_unlift with (lift := mirrorConf) (f := step (M:=MirrorTM)) (h := haltConf (M:=MirrorTM)) in HLoop as (? & HLoop & <- % mirrorConf_injective); auto. - intros ? _. now apply mirror_step. Qed.
imports: Undecidability(TM.Util.Prelim TM.Util.TM_facts)