A maintained weighted-tree append preserves leaves labels root and path writes

For all $\htmlData{mx=2}{A : \htmlData{mx=1}{\htmlData{mx=0}{\operatorname{Type}} \cdot }}$, $\htmlData{mx=1}{h \in \htmlData{mx=0}{\mathbb{N}}}$, $\htmlData{mx=4}{t \in \htmlData{mx=3}{\htmlData{mx=0}{\operatorname{MassTree}}\,\htmlData{mx=1}{A}\,\htmlData{mx=2}{h}}}$, $\htmlData{mx=3}{\mathit{ht} \in \htmlData{mx=2}{\htmlData{mx=0}{\operatorname{valid}}\,\htmlData{mx=1}{t}}}$, $\htmlData{mx=4}{z \in \htmlData{mx=3}{\htmlData{mx=0}{\operatorname{Copies}}\,\htmlData{mx=1}{\operatorname{Bool}}\,\htmlData{mx=2}{h}}}$ and $\htmlData{mx=1}{w \in \htmlData{mx=0}{\mathbb{R}}}$, if $\htmlData{mx=3}{\htmlData{mx=0}{\operatorname{leafWeight}}(\htmlData{mx=1}{t}, \htmlData{mx=2}{z})} \mathrel{\htmlData{mx=4}{=}} 0$ and $0 \mathrel{\htmlData{mx=1}{\leq}} \htmlData{mx=0}{w}$, then