proposition: Lemma universe_inc1 a b: a <o b -> sub (\Po (universe a)) (universe b).
proof: Proof. move /oltP0 => [oa ob ab]. rewrite (universe_rec ob) => t ta; apply /setUf_P; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)