proposition: Lemma stratified_fct_aux_p1 x ( g:= stratified_fct_aux) : ordinalp x -> g x = Lg (stratified_setr x) (fun z => H z (unionf x g)).
proof: Proof. move => ox. rewrite /transdef_ord_prop /g /stratified_fct_aux. rewrite (transdef_ord_pr _ ox) /unionb; aw. apply: Lg_exten => t ts /=; apply: f_equal; set_extens w. move => /setUf_P [y yx]. rewrite LgV// => ha; union_tac. move => /setUf_P [y yx wy]; union_tac; rewrite LgV//. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)