[FOM] query about proving Fermat's last theorem in first-order PA

[Rupert McCallum]

Colin McLarty states in "What does it take to prove Fermat's Last Theorem?" that when one thoroughly understands Wiles' proof of FLT it is clear that in principle the argument can be made to go through in nth-order Peano arithmetic for large finite n, but adapting the argument so that it clearly goes through in first-order PA is far from trivial (he describes how Angus Macintyre has proposed a program for doing this). He also describes how some parts of the argument use cohomological results whose standard proofs make use of a proper class of inaccessible cardinals, but special cases tailored to the specific applications needed can easily enough be seen to go through in Zermelo set theory. 
I was wondering if anyone could point me to a specific part of the proof such that it's definitely not clear how this part of the argument is predicatively justifiable? I am currently trying to understand the proof and would like to identify a point where it's clearly using impredicative reasoning. 
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20190902/74373f75/attachment.html>