proposition: Lemma reductionRL : iPCPb ⪯ PCPb.
proof: Proof. exists id. intro x. now rewrite PCPb_iff_iPCPb. Qed.
imports: List Undecidability.PCP.PCP Undecidability.PCP.Util.Facts Undecidability.PCP.Util.PCP_facts Undecidability.Synthetic.Definitions