proposition: Lemma universe_succ a: ordinalp a -> universe (osucc a) = \Po (universe a).
proof: Proof. move => oa. have asa: a <o osucc a by apply: oltS. apply: extensionality; last by exact:(universe_inc1 asa). rewrite (universe_rec (OS_succ oa)) => t /setUf_P [y ys]. have: y <=o a by apply /oleP. move /universe_inc2 /setP_S; apply. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)