proposition: Lemma tree_rec_def_aux2b i: omega0 <=o i -> tree_stratified i tset.
proof: Proof. move => h x; split; [move => xt; split => // | by case]. move: (NS_tdepth xt) => /(oltP OS_omega) ha. exact: (olt_leT ha h). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)