proposition: Lemma epsilon_fam_pr3 x y: ordinalp x -> epsilon_fam x <o y -> y <=o epsilon_fam (osucc x) -> epsilon_fct y = epsilon_fam (osucc x).
proof: Proof. move => ox. move: (iclosed_fixpoints oopow_normal) => pa. move: (iclosed_col_fs pa ox). rewrite /epsilon_fam/first_derivation. set fx := (ordinalsf _ x); set fy := (ordinalsf _ (osucc x)). move => [fxy ex [ofy ey] etc] l1 l2. move: (epsilon_fct_pr0 (proj31 l2)); set z := (epsilon_fct y). move => [sa sb sc]; apply:oleA; first by apply: sc. have oz:= proj32 sa; have cc1:= (olt_leT l1 sa). by apply: etc. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)