proposition: Lemma well_founded_in_universe x: universe_i x -> well_founded_set x.
proof: Proof. move => ux f ff sf Hf xv. have fu: forall i, natp i -> universe_i (Vf f i). apply: Nat_induction; first by rewrite -xv. by move => n nN /universe_stable_inc HR; exact: (HR _ (Hf _ nN)). have rdec: forall n, natp n -> urank0 (Vf f (csucc n)) <o urank0 (Vf f n). by move => n nN; apply:(urank0_pr3 (fu _ nN) (Hf _ nN)). set A := fun_image Nat (fun z => urank0 (Vf f z)). have oA: ordinal_set A by move => t/funI_P [n /rdec /proj32_1 res ->]. have neA: nonempty A. exists (urank0 (Vf f \0c)); apply/funI_P; exists \0c => //; apply: NS0. move: (ordinal_setI neA oA); set v := intersection A => vA. move/funI_P:vA => [n nN nv]. set t := (urank0 (Vf f (csucc n))). have h: inc t A by apply/funI_P; exists (csucc n) => //; apply:NS_succ. move:(rdec _ nN); rewrite - nv => /olt_i tv. by move: ( (ordinal_irreflexive (oA _ h)) (setI_hi tv h)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)