proposition: Lemma PCPX_derivable P u v : (exists A, A <<= P /\ A <> nil /\ tau1 A = u /\ tau2 A = v) -> derivable P u v.
proof: Proof. intros (A & H1 & H2 & <- & <-). revert H1; pattern A; revert A H2. eapply list_ind_ne; cbn; intros (x,y) H. - simpl_list; constructor 1; auto. - constructor 2; eauto. Qed.
imports: List Undecidability.PCP.PCP Undecidability.PCP.Util.Facts Undecidability.Synthetic.Definitions