proposition: Lemma universe_AF x: universe_i x -> foundation_prop x.
proof: Proof. case: (emptyset_dichot x); first by left. move => [e ex] [a oa xua]; right. set U := fun_image x (urank a). have neU: nonempty U by exists (urank a e); apply /funI_P; ex_tac. have ose: ordinal_set U. move => b /funI_P [z zx ->]. by move: (urank_pr1 oa (universe_trans oa xua zx)) => [/proj31_1]. move:(ordinal_setI neU ose); set y:= intersection U => yU. move: (ose _ yU) => yo. move/funI_P: (yU) => [z zx zu]; ex_tac; apply /set0_P => t /setI2_P [tz tx]. have bu: inc (urank a t) U by apply /funI_P; ex_tac. case: (ordinal_irreflexive (ose _ bu)); apply: (setI_s1 bu). move:(universe_trans oa xua zx) => za. by move: (urank_inc oa za tz)=> [ _]; rewrite - zu => /(oltP yo). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)