proposition: Lemma tree_recdef_pp x: treep x -> tree_rec (Tp x) = h2 (tree_rec x).
proof: Proof. move: card1_nz => n01 ha. move: (proj32 (tdepth_prop_inv) _ ha) => [hb hc]. move: (NS_tdepth ha) => iN. rewrite (tree_recdef_p hb) /tree_rec_prop /Tp; aw; Ytac0; Ytac0; rewrite LgV//. rewrite /tstratified hc (Y_false (@succ_nz _)) (cpred_pr2 iN); Ytac w => //. exact:(proj32 (tdepth1 ha)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)