proposition: Theorem countable_union f: countable_set (domain f) -> (allf f countable_set) -> countable_set (unionb f).
proof: Proof. move=> cs alc; apply /countableP. set d:= domain f. apply: (@cleT (csumb d (fun i => cardinal (Vg f i)))). apply: csum_pr1 =>//. set (h:= cst_graph d aleph0). apply: (@cleT (csumb d (fun i => aleph0))). rewrite/h;apply: csum_increasing; aww. move=> x xd;rewrite !LgV//; move: (alc _ xd) => /countableP //. rewrite csum_of_same - cprod2cr. by apply: cprod_inf1 CIS_aleph0; apply/countableP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)