theorem ocaseeq1 (_z1 _z2: nat) (S: set): $ _z1 = _z2 -> ocase _z1 S == ocase _z2 S $;
_z1 = _z2 -> _z1 = _z2
_z1 = _z2 -> ocase _z1 S == ocase _z2 S