proposition: Lemma countable_indexed_union: forall {X A:Type} (F:IndexedFamily A X), CountableT A -> (forall a:A, Countable (F a)) -> Countable (IndexedUnion F).
proof: Proof. intros. rewrite indexed_to_family_union. apply countable_family_union. - apply countable_img. apply countable_type_ensemble. assumption. - intros. destruct H1. subst. apply H0. Qed.
imports: Coq(Arith ArithRing ClassicalChoice Description FunctionalExtensionality Lia Relation_Definitions Program.Subset QArith ZArith) ZornsLemma(CSB DecidableDec DependentTypeChoice Finite_sets FiniteTypes FunctionPropertiesEns IndexedFamilies InfiniteTypes)