proposition: Lemma derivable_PCPX P u v : derivable P u v -> exists A, A <<= P /\ A <> nil /\ tau1 A = u /\ tau2 A = v.
proof: Proof. induction 1 as [ x y | x y ? ? ? ? (A & ? & ? & ? & ?)]. - exists [(x,y)]; repeat split; cbn; simpl_list; auto; discriminate. - exists ((x,y) :: A); repeat split; simpl; auto; try discriminate; congruence. Qed.
imports: List Undecidability.PCP.PCP Undecidability.PCP.Util.Facts Undecidability.Synthetic.Definitions