proposition: Lemma urank_uniq2 x a b: ordinalp a -> ordinalp b -> inc x (universe a) -> inc x (universe b) -> urank a x = urank b x.
proof: Proof. move => oa ob xa xb; move: (urank_pr1 oa xa) (urank_pr1 ob xb) => [_ s2] [_ s4]. apply: (urank_uniq s2 s4). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)