proposition: Lemma universe_P a: ordinalp a -> forall x, inc x (universe a) <-> exists2 b, b<o a & sub x (universe b).
proof: Proof. move => oa x. rewrite (universe_rec oa); split. by move /setUf_P => [b /(oltP oa) ba /setP_P xb]; exists b. move => [b /(oltP oa) ba /setP_P xb]; union_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)