proposition: Lemma iclosed_normal_ofs (f:fterm): normal_ofs f -> iclosed_proper (fun z => exists2 x, ordinalp x & z = f x).
proof: Proof. move => h. have sb: normal_ofs1 f \0o by apply/normal_ofs_equiv1. move: (iclosed_normal_ofs1 OS0 sb)=> [[pa pb] pc]. have aux: forall z, (exists2 x, ordinalp x & z = f x) <-> exists2 x, \0o <=o x & z = f x. move => z; split; move => [x xp ->]; exists x => //; last by case: xp. exact:(ole0x xp). split => //; first split. + by move => t [x ox ->]; apply(ofs_sincr (proj1 h)). + by move => g pF nef; apply /aux; apply: pb => // x/pF => w; apply/aux. + by move => [E ev]; case:pc; exists E => x; split; [move/ev/aux| move/aux/ev]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)