proposition: Lemma enum_containsL `{falsity_flag} T L : cumulative L -> list_enumerator L T -> list_enumerator (L_con L) (fun A => containsL A T).
proof: Proof. Proof with try (eapply cum_ge'; eauto; lia). intros HL He. split. - induction x as [| phi A]; intros HT. + exists 0. firstorder. + destruct IHA as [m1], (enum_el phi He) as [m2]. 1,2,3: firstorder. exists (1 + m1 + m2). cbn. in_app 2. in_collect (phi, A)... - intros [m]. induction m in x, H0 |-*; cbn in *. + destruct H0 as [<- | []]. firstorder. + invert_list_in. 1: now eapply IHm. apply IHm in H1. apply (enum_p He) in H0. unfold containsL in *. firstorder congruence. Qed.
imports: Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability(FOL.Syntax.Facts FOL.Syntax.Theories) Undecidability(Shared.ListAutomation) Lia