proposition: Lemma enumerable_derivable : enumerable (fun '(C, (u, v)) => @derivable bool C u v).
proof: Proof. eapply list_enumerable_enumerable. eexists. eapply enum_PCP'. Qed.
imports: List Undecidability.PCP.PCP Undecidability.PCP.Util.Facts Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts MoreEnumerabilityFacts ListEnumerabilityFacts) Coq.Init.Wf Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat finite)