proposition: Lemma countable_epsilon x: ordinalp x -> (countable_ordinal x <-> countable_ordinal (epsilon_fam x)).
proof: Proof. move: CIS_omega aleph_oneP => h T. move: (epsilon_fam_pr6 h) => [_ _ [bf _ _] _]. set E := (cnext omega0) in T bf. set f := (Lf epsilon_fam E (Zo E epsilonp)). have ff: function f by move: bf => [[]]. have sf: source f = E by rewrite /f; aw. have tf: target f = (Zo E epsilonp) by rewrite /f; aw. have H: lf_axiom epsilon_fam E (Zo E epsilonp). move => s sE; move: (sE); rewrite - {1} sf => / (Vf_target ff). by rewrite tf /f /Lf /Vf /graph pr1_pair LgV. move => ox; split; first by move /T /H /Zo_S/T. move /T => h1; apply /T. have wa: inc (epsilon_fam x) (target f). by rewrite tf; apply /Zo_P; split => //; apply: epsilon_fam_pr0. move: (proj2 (proj2 bf) _ wa); aw; move => [a ae]; rewrite LfV// => eq. move/(cnextP (proj1 h)):(ae) => [oa _]. move: epsilon_fam_pr5 => [ii _]. by case:(oleT_ell ox oa); first (by move => ->); move /ii =>[]; rewrite eq. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)