proposition: Lemma Mirror_RealiseIn R (k : nat) : pM ⊨c(k) R -> Mirror ⊨c(k) Mirror_Rel R.
proof: Proof. intros H. eapply Realise_total. split. - eapply Mirror_Realise. now eapply Realise_total. - eapply TerminatesIn_monotone. + eapply Mirror_Terminates. now eapply Realise_total. + firstorder. Qed.
imports: Undecidability(TM.Util.Prelim TM.Util.TM_facts)