proposition: Lemma urank_alt1 a x: ordinalp a -> inc x (universe a) -> urankA a x = osucc (urank a x).
proof: Proof. move => oa xa. move: (proj2 (urankA_pr oa xa)) => h2. move:(urank_pr oa (universe_trans oa xa))=> [_ ] /urank_alt h1. exact:(urankA_uniq h2 h1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)