proposition: Lemma well_founded_universe a: ordinalp a -> forall x, inc x (universe a) <-> (well_founded_set x /\ exists2 b , b<o a & urank_prop x b).
proof: Proof. move=> oa; split. move => xa; split. by apply: (well_founded_in_universe); exists a. by move: (urank_pr1 oa xa)=> [sa sb]; exists (urank a x). by move => [sa [b /universe_inc1 lba [ob /setP_P sb _]]]; apply: lba. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)