proposition: Lemma tree_rec_def_aux2c i: i <o omega0 -> i <> \0c -> tree_stratified i (tset_index (cpred i)).
proof: Proof. move => ii inz. move/(oltP OS_omega): ii => iN. move: (cpred_pr iN inz) => [ha hb]. move => x; split => xE. split; first by apply/tsetP; exists (cpred i). by apply: oclt; rewrite hb; apply /(cltSleP ha); apply:tdepth3. move: xE =>[ xE dx]. apply:(tdepth2 xE ha); apply /(cltSleP ha); rewrite - hb. by apply: (oclt3 (CS_nat (NS_tdepth xE)) (CS_nat iN)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)