proposition: Lemma enumerable_conj X (p q : X -> Prop) : discrete X -> enumerable p -> enumerable q -> enumerable (fun x => p x /\ q x).
proof: Proof. intros [] % discrete_iff [Lp] % enumerable_enum [Lq] % enumerable_enum. eapply enumerable_enum. exists (fix f n := match n with 0 => [] | S n => f n ++ (filter (fun x => Dec (In x (cumul Lq n))) (cumul Lp n)) end). intros x. split. + intros []. eapply (list_enumerator_to_cumul H) in H1 as [m1]. eapply (list_enumerator_to_cumul H0) in H2 as [m2]. exists (1 + m1 + m2). cbn. apply in_or_app. right. apply filter_In. split. * eapply cum_ge'; eauto; lia. * eapply Dec_auto. eapply cum_ge'; eauto; lia. + intros [m]. induction m. * inversion H1. * apply in_app_iff in H1. destruct H1 as [?|H1]; [now auto|]. apply filter_In in H1. destruct H1 as [? H1]. split. ** eapply (list_enumerator_to_cumul H). eauto. ** destruct (Dec _) in H1; [|easy]. eapply (list_enumerator_to_cumul H0). eauto. Qed.
imports: Undecidability.Synthetic(DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts) Undecidability.Shared(Dec) List