proposition: Lemma urankA_succ x a: urankA_prop x a -> osuccp a.
proof: Proof. move => [oa xa etc]. case: (ordinal_limA oa) => // hc. - by move: xa; rewrite hc; rewrite universe_0 => /in_set0. - by move: xa; rewrite (universe_limit hc) => /setUf_P [y /(oltP oa) /etc]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)