proposition: Lemma urank_universe a: ordinalp a -> urank_prop (universe a) a.
proof: Proof. move => ap; split => // c /universe_inc1 ca su. move: (sub_smaller (sub_trans ca su)); rewrite card_setP - cpowcr => sa. case: (cltNge (cantor (CS_cardinal (universe c))) sa). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)