Item
3.3.8.b
.
\(\forall x \forall y \forall z (z = x+y \wedge \forall w (x-y \ne w))\text{.}\)
in-context