for T, T9 being DecoratedTree
for p, q being Element of dom T st not p is_a_prefix_of q holds
(T with-replacement (p,T9)) . q = T . q