proposition: Lemma card_universe_fin n: natp n -> finite_set (universe n).
proof: Proof. move: n; apply: Nat_induction. by rewrite universe_0; apply: emptyset_finite. move => n nN /card_finite_setP Hrec. rewrite (succ_of_nat nN) (universe_succ (OS_nat nN)). apply /card_finite_setP; rewrite card_setP - cpowcr; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)