proposition: Lemma reductionLR : PCPb ⪯ iPCPb.
proof: Proof. exists id. exact PCPb_iff_iPCPb. Qed.
imports: List Undecidability.PCP.PCP Undecidability.PCP.Util.Facts Undecidability.PCP.Util.PCP_facts Undecidability.Synthetic.Definitions