Actually, bugs might surface during such restructuring. If the statement you're proving can be greatly simplified to something reasonable, if we omit this one weird special case, that indicates a bug in the specification.