proposition: Lemma urank_alt x b: urankA_prop x (osucc b) <-> urank_prop x b.
proof: Proof. split. move => [pa pb pc]. have ob: ordinalp b by apply: OS_succr. split => //; first by apply/setP_P; rewrite - (universe_succ ob). move => c cb /setP_P h. have oc:=proj31_1 cb. by move /oltSSP: cb => /pc; rewrite (universe_succ). move => [ob pb pc]; move: (OS_succ ob) => osb. have ha: inc x (universe(osucc b)) by rewrite (universe_succ ob); apply/setP_P. have: universe_i x by exists (osucc b). move /urankA_ex => [c oc h]; move: (h) => [qa qb qc]. move: qb; rewrite (universe_succ oc) => /setP_P => qb. case: (oleT_ell ob oc); [by move => -> | | by move /pc]. by move /oltSSP => /qc. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)