proposition: Lemma enumerable_disj X (p q : X -> Prop) : enumerable p -> enumerable q -> enumerable (fun x => p x \/ q x).
proof: Proof. intros [Lp H] % enumerable_enum [Lq H0] % enumerable_enum. eapply enumerable_enum. exists (fix f n := match n with 0 => [] | S n => f n ++ (Lp n) ++ (Lq n) end). intros x. split. - intros [H1 | H1]. * eapply H in H1 as [m]. exists (1 + m). cbn. apply in_or_app. right. apply in_or_app. now left. * eapply H0 in H1 as [m]. exists (1 + m). cbn. apply in_or_app. right. apply in_or_app. now right. - intros [m]. induction m. * inversion H1. * apply in_app_iff in H1. destruct H1 as [?|H1]; [now auto|]. apply in_app_iff in H1. unfold list_enumerator in *; firstorder easy. Qed.
imports: Undecidability.Synthetic(DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts) Undecidability.Shared(Dec) List