proposition: Lemma MPCP_PCP_cor : MPCP (x0/y0, R) <-> PCP P.
proof: Proof. split. - intros (A & Hi & (B & HiB & H) % MPCP_PCP). + exists (d :: B). firstorder try congruence. cbn. f_equal. now rewrite H. + eassumption. - intros ([|d' B] & Hi & He & H); firstorder. pose proof H as -> % match_start; eauto. cbn -[fresh] in H. inv H. eapply PCP_MPCP in H1; cbn. + eassumption. + eapply cons_incl. eassumption. + apply incl_appl. apply incl_refl. + apply incl_appr. apply incl_appl. apply incl_refl. Qed.
imports: Bool List Undecidability.PCP.PCP Undecidability.PCP.Util.Facts Undecidability.PCP.Util.PCP_facts Undecidability.Synthetic.Definitions