proposition: Lemma iclosed_fixpoints (f:fterm): normal_ofs f -> iclosed_proper (fun z => ordinalp z /\ f z = z).
proof: Proof. move => nf; split; last first. apply:unbounded_non_coll => x ox. move: (normal_ofs_fix nf ox) => [pa pb _]; have [_ oo _]:= pa. by exists (the_least_fixedpoint_ge f x). split; [by move => t [] | move => F fp nef ]. move /normal_ofs_equiv1: (nf) => [pa pb]. have pc: (forall x, inc x F -> \0o <=o x) by move =>x /fp [/ole0x ox _]. have pd: (fun_image F f) = F. set_extens t. by move => /funI_P [z zf ->]; rewrite (proj2 (fp _ zf)). by move => tf; apply /funI_P; ex_tac; rewrite (proj2 (fp _ tf)). move: (pb _ pc nef); rewrite pd => h; split => //; apply: OS_sup. by move => t /pc []. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)