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 it-
self 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 com-
fortable sharing this formalization as-is.)

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