Comment by thom

Hidden like any subtle bug that one might gloss over when inspecting the source code. The statement you’re trying to prove could be thousands of lines long and that semantic mismatch could occur anywhere. We seem to be very blasé about this.