for x, y being object
for p, q being DTree-yielding FinSequence st x -tree p = y -tree q holds
( x = y & p = q )