for x, y being object
for p, q being FinSequence st x -flat_tree p = y -tree q & q is DTree-yielding holds
( x = y & len p = len q & ( for i being Nat st i in dom p holds
q . i = root-tree (p . i) ) )