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