proposition: Lemma tree_recdef_pb' n: natp n -> tree_rec (Tb n) = h1 n.
proof: Proof. move => h. have xt:= TS_base h. by rewrite (tree_recdef_p xt) /tree_rec_prop pr1_pair pr2_pair; Ytac0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)