theorem recneq1 (_z1 _z2: nat) (S: set) (n: nat): $ _z1 = _z2 -> recn _z1 S n = recn _z2 S n $;
_z1 = _z2 -> _z1 = _z2
_z1 = _z2 -> recn _z1 S n = recn _z2 S n