proposition: Lemma epsilon_fam_pr4 x: ordinalp x -> epsilon_fam (osucc x) = epsilon_fct (osucc (epsilon_fam x)).
proof: Proof. apply: first_derivation_p3;apply: oopow_normal. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)