proposition: Lemma countable_family_union: forall {X:Type} (F:Family X), Countable F -> (forall U, In F U -> Countable U) -> Countable (FamilyUnion F).
proof: Proof. intros. destruct (choice_on_dependent_type (fun (a : { U | In F U }) (f:{x:X | In (proj1_sig a) x} -> nat) => injective f)) as [choice_fun_inj]. { intros [U]. destruct (H0 U) as [f]; try assumption. now exists f. } destruct (choice (fun (x:{x:X | In (FamilyUnion F) x}) (a: { U | In F U }) => In (proj1_sig a) (proj1_sig x))) as [choice_fun_a]. { destruct x as [x [a]]. now exists (exist _ a i). } destruct countable_nat_product as [g], H as [h]. exists (fun x:{x:X | In (FamilyUnion F) x} => g (h (choice_fun_a x), choice_fun_inj _ (exist _ _ (H2 x)))). intros x1 x2 H4. apply H3 in H4. injection H4 as H5 H6. apply H in H5. revert H6. generalize (H2 x1), (H2 x2). rewrite H5. intros. apply H1 in H6. injection H6. destruct x1, x2. apply subset_eq_compat. 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)