theorem ocasepeq1 (_z1 _z2: wff) (S: set): $ (_z1 <-> _z2) -> ocasep _z1 S == ocasep _z2 S $;
(_z1 <-> _z2) -> (_z1 <-> _z2)
(_z1 <-> _z2) -> ocasep _z1 S == ocasep _z2 S