proposition: Lemma tstratified_val i: ordinalp i -> stratified_set treep tdepth i = tstratified i.
proof: Proof. move => oi. have H:= (stratified_setP tree_rec_def_aux2 oi); rewrite /tstratified. case: (equal_or_not i \0c) => iz; Ytac0. apply/set0_P => x; case/(stratified_setP tree_rec_def_aux2 oi) => _. by rewrite iz;move /olt0. case:(oleT_el OS_omega oi) => ii. Ytac0; move:(tree_rec_def_aux2b ii)=> ww. set_extens t; first by move/(stratified_setP tree_rec_def_aux2 oi) => /ww. by move/ww/(stratified_setP tree_rec_def_aux2 oi). rewrite (Y_false (oltNge ii)); move:(tree_rec_def_aux2c ii iz)=> ww. set_extens t; first by move/(stratified_setP tree_rec_def_aux2 oi) => /ww. by move/ww/(stratified_setP tree_rec_def_aux2 oi). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)