proposition: Lemma sub_Nat_Vomega: sub Nat (universe omega0).
proof: Proof. move => t tb. move: (urank_ordinal (OS_nat tb))=> /urank_alt [pa pb _]. move: omega_limit => /limit_ordinal_P [_ h]. have to: t <o omega0 by apply /(oltP OS_omega). exact:(universe_inc2 (proj1 (h _ to)) pb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)