proposition: Lemma tdepth3 x m: natp m -> inc x (tset_index m) -> (tdepth x) <=c m.
proof: Proof. move => sa sb. have ts: treep x by apply/tsetP; exists m. by move: (tdepth1 ts) => [sc sd se]; exact: (se _ sa sb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)