proposition: Lemma tdepth4 x: treep x -> tdepth x = \0c -> inc x tset_base.
proof: Proof. by move => /tdepth1 [_ sa _] sb; move: sa; rewrite sb tset_index0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)