proposition: Lemma epsilon_fam_pr0 x: ordinalp x -> epsilonp (epsilon_fam x).
proof: Proof. move: (iclosed_fixpoints oopow_normal) => [pa pb]. by move:(ordinals_col_p1 (proj1 pa) pb) => [na _ _ _ _]; move /na. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)