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