proposition: Lemma iclosed_fixpoints_fun f a : ordinalp a -> normal_function f a a -> iclosed_set (fixpoints f).
proof: Proof. move => oa na; move:(na) => [[ff sf tf] pb pc]. rewrite /fixpoints sf; set E := Zo a _. have ose: ordinal_set E by move =>t /Zo_S /(Os_ordinal oa). split => // F fp nef. have subfa: sub F a by move => t /fp /Zo_S. have l1:= (ord_sup_M fp ose). have h: \osup E <=o a by apply:ord_ub_sup1 => //; apply : Zo_S. have l2:= (oleT l1 h). case: (equal_or_not (\osup F) a) => sna. by rewrite - sna in h; left; apply:oleA. case: (normal_function_equiv oa oa na subfa nef) => //. have ->: (Vfs f F) = F. have aux: sub F (source f) by ue. set_extens t. by move => /(Vf_image_P ff aux) [z zf ->]; rewrite (Zo_hi (fp _ zf)). by move => zf; apply /(Vf_image_P ff aux); ex_tac; rewrite (Zo_hi (fp _ zf)). by move => fxp;right; apply: Zo_i => //; apply /(oltP oa). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)