proposition: Lemma urank0_pr a x (r:= urank0 x): ordinalp a -> inc x (universe a) -> r = urank a x /\ urank_prop x r.
proof: Proof. move => oa xua. pose p z := exists a, [/\ ordinalp a, inc x (universe a) & z = urank a x]. have pa: (exists z, p z) by exists (urank a x); exists a; split => //. move: (choose_pr pa); rewrite /r/urank0 -/p. set v := choose p; move => [b [ob xub zv]]. rewrite(urank_uniq2 oa ob xua xub); split => //. have ha: sub x (universe b). apply /setP_P; rewrite - (universe_succ ob). by apply: (universe_inc2 (proj1 (oltS ob))). rewrite zv;exact: (proj2 (urank_pr ob ha)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)