proposition: Lemma universe_omega_HF x: inc x (universe omega0) <-> hereditarily_finite x.
proof: Proof. split; last first. move => [rf [n nb]]; move: n nb x rf. apply: Nat_induction. move => x rd; rewrite (proj1 (rept_union_pr x)) => ->. apply: universe_omega_hi; [apply:emptyset_finite | apply: sub0_set]. move => n nN Hrec x recf fn. move: (rept_union_pr x) => [pa pb]; apply: universe_omega_hi. by move: (recf _ NS0); rewrite pa. move => t tx; move:(rept_union_inc tx nN); rewrite fn=> /sub_set0;apply: Hrec. move:(rept_union_inc tx) => aux. move => k kN; exact: (sub_finite_set (aux _ kN) (recf _ (NS_succ kN))). move => h. move: (rept_union_pr x) => [pa pb]. have aux: forall n, inc n Nat -> (inc (rept_union x n) (universe omega0)). apply: Nat_induction; first by rewrite pa. by move => n nN; move /(urank_union OS_omega)=> []; rewrite (pb _ nN). split; first by move => n /aux /universe_omega_props []. move:(proj33 (universe_omega_props h)); set n := urank _ _ => nN. have rec: forall k, inc k Nat -> k <=c n -> urank omega0 (rept_union x k) = n -c k. apply: Nat_induction; first by rewrite pa (cdiff_n0 nN). move => k kN Hrec skn. move: (urank_union OS_omega (aux _ kN)) => [_]; rewrite - (pb _ kN). suff: union (n -c k) = n -c csucc k. by move <-; rewrite (Hrec (cleT (proj1 (cltS kN)) skn)). move: (cdiff_pr skn); set c := n -c (csucc k). have cN: natp c by rewrite /c; fprops. rewrite (csum_Sn _ kN) -(csum_nS _ cN) csumC => h1. rewrite (cdiff_pr2 (NS_succ cN) kN h1) (succ_of_nat cN) [union _]succo_K //. by apply: OS_nat. move: (urank_pr1 OS_omega (aux _ nN)). move: (rec _ nN (cleR (CS_nat nN))); rewrite cdiff_nn => ->. by move => [_ [_]]; rewrite universe_0 => /sub_set0 sa _;exists n. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)