proposition: Lemma enum_tprv {p : peirce} {b : falsity_flag} T L : list_enumerator L T -> list_enumerator (L_tded (cumul L)) (tprv T).
proof: Proof. Proof with try (eapply cum_ge'; eauto; lia). intros He. assert (HL : list_enumerator (cumul L) T) by now apply list_enumerator_to_cumul. split. - intros (A & [m1] % (enum_el A (@enum_containsL _ _ (cumul L) (to_cumul_cumulative L) HL)) & [m2] % (enum_el x (enum_prv A))). exists (1 + m1 + m2). cbn. in_app 2. eapply in_concat. eexists. split. 1: eapply in_map_iff; eexists; repeat split. 2: idtac... idtac... - intros [m]. induction m in x, H |-*; cbn in *. 1: contradiction. invert_list_in. 1: now apply IHm. exists x1. split. + eapply (enum_p (enum_containsL (to_cumul_cumulative L) HL)); eauto. + eapply (enum_p (enum_prv x1)); eassumption. Qed.
imports: Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability(FOL.Syntax.Facts FOL.Syntax.Theories) Undecidability(Shared.ListAutomation) Lia