proposition: Lemma PCPb_iff_BPCP P : PCPb P <-> BPCP P.
proof: Proof. unfold PCPb; rewrite PCPX_iff_dPCP; split. - intros (u & Hu); constructor 1 with u; trivial. - intros (u & Hu); exists u; trivial. Qed.
imports: List Undecidability.PCP.PCP Undecidability.PCP.Util.Facts Undecidability.PCP.Reductions.PCPX_iff_dPCP Undecidability.Synthetic.Definitions