proposition: Lemma AF_universe x: universe_i x.
proof: Proof. move: (tc_exists x) => []; set b1 := (transitive_closure x) => tb xb etc. set b:= Zo b1 (fun z => ~(universe_i z)). case: (AF b). move => be; apply /universe_stable_inc => y yx; ex_middle bad. by empty_tac1 y; apply: Zo_i => //; apply: xb. move => [y yb ye]; move: (Zo_S yb) => yb1. move: (Zo_hi yb) => yne. have [u uy nuu]: exists2 u, inc u y & ~ (universe_i u). ex_middle nxu; case: yne; apply /universe_stable_inc => s sx. ex_middle bad1; case: nxu; ex_tac. by empty_tac1 u; apply:Zo_i => //; apply: (tb y). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)