Here is the code for the paper "A simple formalization of alpha-equivalence" by Kalmer Apinis and Danel Ahman (submitted to LMCS) Proofs in file Lam.v. Compile with make. Tested with The Rocq Prover, version 9.1.0 and rocq-equations 1.3.1+9.1.