proposition: Lemma Spsi_p1' a b (b' := (Yo (Spsi_aux a b) (osucc b) b)): ordinalp a -> ordinalp b -> b' <o Sphi a b'.
proof: Proof. move => oa ob. have ob':ordinalp b' by rewrite /b'; Ytac h; fprops. by apply: (Spsi_p1 oa ob ob'). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)