proposition: Theorem reduction : SR ⪯ MPCP.
proof: Proof. exists (fun '(R, x, y) => (d R x y, P R x y)). intros [[R x] y]. unfold SR. rewrite SR_MPCP_cor. unfold MPCP. unfold d. firstorder trivial. Qed.
imports: List Undecidability.PCP.PCP Undecidability.PCP.Util.Facts Undecidability.PCP.Util.PCP_facts Undecidability.StringRewriting.SR Undecidability.StringRewriting.Util.Definitions Undecidability.Synthetic.Definitions