So here is the problem -- we have two constructions of -z.

Whether or not this shows up in a tree somewhere if you try to compose functions together is probably undecideable.

Either they aren't equal and you've broken any tree that includes that construction of -z anywhere in it, _or_ you have two trees which _are_ equal, but disagree on their value at every point

Any rule that tries to rewrite one form to the other is unsound

The lack of any equational theory makes a lot of claims about it fairly nonsensical.