proposition: Lemma universe_limit a: limit_ordinal a -> universe a = unionf a universe.
proof: Proof. move => [pa pb pc]; apply extensionality. move => t /(universe_P pa) [b /(oltP pa) ba /setP_P etc]. apply /setUf_P; exists (osucc b); first by apply: pc. rewrite universe_succ //; exact (Os_ordinal pa ba). by move => t /setUf_P [y /(oltP pa) [ya _]]; apply: (universe_inc2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)