proposition: Theorem reduction : MPCP ⪯ PCP.
proof: Proof. exists (fun '(x, y, R) => P R x y). intros ((x & y) & R). eapply MPCP_PCP_cor. Qed.
imports: Bool List Undecidability.PCP.PCP Undecidability.PCP.Util.Facts Undecidability.PCP.Util.PCP_facts Undecidability.Synthetic.Definitions