proposition: Lemma all_der_p2 x: ordinalp x -> g x \0o = f x.
proof: Proof. move => ox. have [sb sc sd se sf]:= (all_der_bound_prop ox OS0 bf). have sa:= (all_der_bound_prop2 ox OS0). rewrite se in sa. move:(many_der_ex sb sa) => [pa pb pc _ _]. move: (f_equal (Vf^~ x) pc); rewrite - se LfV//. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)