proposition: Lemma enum_PCP' : list_enumerator L_PCP (fun '(C, (u, v)) => @derivable bool C u v).
proof: Proof. intros ( C & u & v ). split. + induction 1. * destruct (el_T C) as [m1], (el_T x) as [m2], (el_T y) as [m3]. exists (1 + m1 + m2 + m3). cbn. in_app 2. in_collect (C, x, y); eapply cum_ge'; eauto; lia. * destruct IHderivable as [m1], (el_T x) as [m2], (el_T y) as [m3]. exists (1 + m1 + m2 + m3). cbn. in_app 3. in_collect ( (C, (u, v), x, y)); eapply cum_ge'; eauto; try lia. + intros [m]. revert C u v H. induction m; intros. * inv H. * cbn in H. invert_list_in. 1: eauto. 1: econstructor; congruence. destruct p as (p1 & p2 & p3). destruct Dec; try congruence. injection H; intros <- <- <-. eapply der_cons; eauto. 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)