mzero package:fin

Convert from zero+succ to refl+step definition. Inverse of toZeroSucc.