proposition: Lemma urankA_ex x: universe_i x -> exists2 b, ordinalp b & urankA_prop x (osucc b).
proof: Proof. move => [a oa xa]; move: (urankA_pr oa xa) => [_ pb]. move /urankA_succ: (pb) => [b ob bs]; rewrite bs in pb; exists b => //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)