proposition: Lemma all_der_bound_prop2 x i: ordinalp x -> ordinalp i -> normal_function (Lf f (b x i) (b x i)) (b x i) (b x i).
proof: Proof. move => sa sb; move: (all_der_bound_prop sa sb bf). move => [ta tb tc td te]. rewrite td in te. by move:(normal_ofs_restriction ta nf te); rewrite - td. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)