proposition: Lemma first_derivation_p0 (f: fterm): normal_ofs f -> normal_ofs (first_derivation f).
proof: Proof. move /iclosed_fixpoints => pa; exact: (ordinals_col_p2 pa). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)