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.
Especially when "this one weird special case" pulls in the entire binary layout because your code has a hole that allows an attacker to jump to a specified address