proposition: Lemma urank_ex x: universe_i x -> exists b, urank_prop x b.
proof: Proof. move => [a oa xa]; exists (urank a x). by move: (universe_trans oa xa) => /(urank_pr oa) [_ h]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)