proposition: Lemma tree_recdef_pb x: inc x tset_base -> tree_rec x = h1 (Q x).
proof: Proof. move => ha. have xt:= (tset_base_hi ha). by move/tset_baseP: ha => [n nN ->]; rewrite (tree_recdef_pb' nN) /Tb; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)