proposition: Lemma tree_recdef_px x y: treep x -> treep y -> tree_rec (Tx x y) = h3 (tree_rec x) (tree_rec y).
proof: Proof. move: card1_nz => n01 ha ha'. move: card_12 card2_nz => c12 c02. move: (proj33 (tdepth_prop_inv) _ _ ha ha') => [hb hc]. move: (NS_tdepth ha) (NS_tdepth ha') => iN iN'. case: (Nmax_p1 iN iN'). set m := (cmax (tdepth x) (tdepth y)) => mN max1 max2. have ra: inc x (tstratified (tdepth (Tx x y))). rewrite /tstratified hc (Y_false (@succ_nz _)); Ytac w => //. by move: (tdepth2 ha mN max1); rewrite (cpred_pr2 mN). have rb: inc y (tstratified (tdepth (Tx x y))). rewrite /tstratified hc (Y_false (@succ_nz _)); Ytac w => //. by move: (tdepth2 ha' mN max2); rewrite (cpred_pr2 mN). rewrite (tree_recdef_p hb) /tree_rec_prop /Tx; aw; Ytac0; Ytac0; rewrite !LgV//. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)