for p being FinSequence st p is Tree-yielding holds
elementary_tree (len p) c= tree p