proposition: Lemma universe_inaccessible_card2: cardinal(universe a) = a.
proof: Proof. move: (ia) => [[ [ica _] _] _]. move:(infinite_card_limit2 ica) => loa. move:(proj31 loa) => oa. move: (card_card (proj1 ica)) => caa. apply cleA; last first. by move: (urank_ordinal oa)=> [ _ /sub_smaller]; rewrite caa. rewrite (universe_rec oa). set yy := unionf _ _. have ->: yy = unionb (Lg a (fun z => \Po (universe z))). set_extens t. move /setUf_P => [s sa sb]; apply /setUb_P; aw; ex_tac; rewrite LgV//. move => /setUb_P; aw; move => [s sa]; rewrite LgV// => sb. by apply /setUf_P; ex_tac. move: (csum_pr1 (Lg a (fun z => \Po (universe z)))) => h. apply: (cleT h); set s := csumb _ _; clear h. set f := Lg a (fun z => cardinal(\Po (universe z))). have pra: csum f = s. rewrite /s /f; aw; apply:csumb_exten; move => t ty /=; rewrite LgV//. have prb: domain f = a by rewrite /f;aw. have prc: cardinal_fam f by move => t; rewrite prb /f => ys; rewrite LgV; fprops. have prd: fgraph f by rewrite /f; fprops. have pre: forall i : Set, inc i (domain f) -> Vg f i <c a. move => i; rewrite prb /f => iy; rewrite LgV// card_setP. move: (iy) => /(oltP oa) iy'. rewrite - cpowcr; exact: (proj2 ia _ (universe_inaccessible_card1 iy')). move: (csum_of_small_b2 (conj prd pre)). by rewrite prb pra (csquare_inf ica). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)