proposition: Lemma normal_ofs_restriction f C (E := cnext C): infinite_c C-> normal_ofs f -> (forall x, inc x E -> inc (f x) E) -> normal_function (Lf f E E) E E.
proof: Proof. move => ice [nfa nfb] Esf. have ff: function (Lf f E E) by apply: lf_function. have fp: function_prop (Lf f E E) E E by saw. have si: sincr_ofn (Lf f E E) E by move => a b aE bE /nfa; rewrite !LfV. split => // a ae /nfb la; rewrite LfV // la; congr union. have asE: sub a E. have oe: ordinalp E by exact : (proj1 (CS_cnext (proj1 ice))). move => t ta; exact:(ordinal_transitive oe ae ta). have asf: sub a (source (Lf f E E)) by aw. set_extens t. move/funI_P => [z za ->]; apply /(Vf_image_P ff asf);ex_tac. by rewrite LfV//;apply: asE. move/(Vf_image_P ff asf) => [u ua]; move:(asE _ ua) => uE; aw => ->. rewrite LfV//; apply /funI_P; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)