I was using Isabelle. There is indeed a paper about this: http://link.springer.com/chapter/10.1007%2F11921240_19 http://link.springer.com/chapter/10.1007%2F1192

I was using Isabelle. There is indeed a paper about this: http://link.springer.com/chapter/10.1007%2F11921240_19 http://link.springer.com/chapter/10.1007%2F11921240_19, and the flaw is described on page 284.