See the 2021-present work of [Joshua Grosso](https://jgrosso.github.io/), who [formalised the paper in Coq](https://github.com/jgrosso/coq-alpha-pearl), correcting some errors in the process (last update 3 weeks ago). However, Grosso wrote:

>To our knowledge, all of the main results contained within the paper itself have been formalized. (Proving equivalence to de Bruijn terms is still in progress, but because it is left to the reader in the original paper, we are comfortable sharing this formalization as-is.)

So it might be that with the improved treatment the desired equivalence is easier to show?