proposition: Lemma tree_rec_def_aux2: forall i, ordinalp i -> exists E, tree_stratified i E.
proof: Proof. move => i oi; case:(oleT_el OS_omega oi) => ii. by exists tset; apply:tree_rec_def_aux2b. case: (equal_or_not i \0c) => inz. exists emptyset; by rewrite inz;apply:tree_rec_def_aux2a. by exists (tset_index (cpred i)); apply: tree_rec_def_aux2c. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)