proposition: Lemma countable_union: forall {X A:Type} (F:IndexedFamily A X), CountableT A -> (forall a:A, Countable (F a)) -> Countable (IndexedUnion F).
proof: Proof. intros. destruct (choice_on_dependent_type (fun (a:A) (f:{x:X | In (F a) x} -> nat) => injective f)) as [choice_fun_inj]. - intro. destruct (H0 a). now exists f. - destruct (choice (fun (x:{x:X | In (IndexedUnion F) x}) (a:A) => In (F a) (proj1_sig x))) as [choice_fun_a]. + destruct x as [x [a]]. now exists a. + destruct countable_nat_product as [g], H as [h]. exists (fun x:{x:X | In (IndexedUnion 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: FiniteTypes Relation_Definitions ZArith QArith IndexedFamilies InfiniteTypes CSB DecidableDec FunctionalExtensionality ProofIrrelevance DependentTypeChoice ClassicalChoice Arith ArithRing