See the 2021-present work of Joshua Grosso, who formalised the paper in Coq, 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?