proposition: Lemma normal_ofs_equiv2 f a: ordinalp a -> normal_ofs f -> normal_ofs1 f a.
proof: Proof. move=> oa; move /normal_ofs_equiv1 => [p2 p3]; split => //. move=> x y xp yp; apply: p2 =>//; apply: (ole0x (proj32 xp)). move=> X xp xX; rewrite p3 //. move=> t tx; exact: (ole0x (proj32 (xp _ tx))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)