for T, T1 being DecoratedTree
for t being Element of dom T holds tree (T,{t},T1) = T with-replacement (t,T1)