Comment by js8

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.