proposition: Lemma universe_mo' a (U :=fun z => inc z (universe a)) : ordinalp a -> ( (forall x y, U x -> inc y x -> U y) /\ (forall x y, U x -> sub y x -> U y)).
proof: Proof. move => oa. rewrite /U; split; first by move => x y xy; apply: (universe_trans oa). by move => x y xua /(urank_sub oa xua) []. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)