proposition: Lemma universe_inaccessible_bis a : inaccessible a -> cardinal (universe a) = a.
proof: Proof. move => ia. have ica := (proj1 (proj1 (proj1 ia))). have {1} <- : omega0 +o a = a. apply: (indecomp_prop1 (cardinal_indecomposable ica)). exact: (oclt (inaccessible_uncountable (proj1 ia))). rewrite (card_universe (proj1 (proj1 ica))). exact: (beth_inaccessible1 ia). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)