proposition: Lemma epsilon_fam_pr1 y: epsilonp y -> exists2 x, ordinalp x & y = epsilon_fam x.
proof: Proof. move: (iclosed_fixpoints oopow_normal) => [pa pb]. move:(ordinals_col_p1 (proj1 pa) pb) => [_ na _ _ _];apply:na. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)