for t1, t2 being finite DecoratedTree st t1 in Subtrees t2 holds
height (dom t1) <= height (dom t2)