proposition: Lemma countable_bunion A (s : A -> Prop) B (ss : A -> B -> Prop) (K : countable s) (L : forall a, countable (ss a)) : countable (⋃₁x ∈ s, ss x).
proof: Proof. tertium_non_datur (inhabited B) as [Ib|NIb]; vauto. unfold countable in K, L; desf; vauto. destruct Ib as [b]; eapply surjection_countable with (f := fun _ => b). unfold set_bunion; ins; desf; destruct K; vauto. assert (C: exists f : A -> nat -> B, forall a, enumerates (f a) (ss a)). { apply choice with (R := fun x y => enumerates y (ss x)). intros x; specialize (L x); desf; eauto. } clear L; desc. assert (D := fun x => enumerates_surjection (C x)); clear C. specialize (enumerates_surjection K); clear K; intro K. apply surjection_countable with (f := fun n => f (nu (nat_fst n)) (nat_snd n)). unfold set_bunion; ins; desc. apply K in IN; desf. apply D in IN0; desf. by eexists (nat_tup _ _); rewrite nat_fst_tup, nat_snd_tup. Qed.
imports: Arith micromega.Lia Setoid IndefiniteDescription ClassicalChoice HahnBase HahnList HahnEquational HahnRewrite HahnRelationsBasic HahnSets HahnNatExtra HahnListBefore HahnWf HahnSorted HahnTotalExt