proposition: Lemma iPCPb_undec : undecidable iPCPb.
proof: Proof. apply (undecidability_from_reducibility PCPb_undec). exists id. exact PCPb_iff_iPCPb.PCPb_iff_iPCPb. 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