theorem zaddeq2d (_G: wff) (m _n1 _n2: nat): $ _G -> _n1 = _n2 $ > $ _G -> m +Z _n1 = m +Z _n2 $;
_G -> m = m
_G -> _n1 = _n2
_G -> m +Z _n1 = m +Z _n2