proposition: Lemma MPCP_undec : undecidable MPCP.
proof: Proof. apply (undecidability_from_reducibility SR_undec.SR_undec). exact SR_to_MPCP.reduction. Qed.
imports: Undecidability.PCP.PCP Undecidability.Synthetic.Undecidability Undecidability.Synthetic.ReducibilityFacts Undecidability.FRACTRAN(FRACTRAN Reductions.MM_FRACTRAN) Undecidability.MinskyMachines(MM Reductions.BSM_MM) Undecidability.StackMachines(BSM Reductions.SBTM_HALT_to_HaltBSM) Undecidability.TM.SBTM_undec