proposition: Corollary SR_MPCP_cor : x0 ≻* y0 <-> exists A, A <<= P /\ tau1 (d :: A) = tau2 (d :: A).
proof: Proof. split. - intros ?. cbn in H. eapply SR_MPCP in H as (A & ? & ?). { exists A. firstorder. cbn. rewrite H0. cbn. now simpl_list. } eapply incl_appl. apply incl_refl. - intros (A & ? & ?). eapply MPCP_SR with (y := []) (A := A); try trivial. { eapply incl_appl. now apply incl_refl. } inv H0. rewrite H2. now simpl_list. 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