proposition: Lemma reductionLR : PCPb ⪯ BPCP.
proof: Proof. exists id; exact PCPb_iff_BPCP. Qed.
imports: List Undecidability.PCP.PCP Undecidability.PCP.Util.Facts Undecidability.PCP.Reductions.PCPX_iff_dPCP Undecidability.Synthetic.Definitions