By "modulo alpha conversion" I understand you to mean that the functionality was the same, only the names changed in some cases. A clearer way to put this would

By "modulo alpha conversion" I understand you to mean that the functionality was the same, only the names changed in some cases. A clearer way to put this would be to talk about "equivalence" or maybe even isomorphism? I'm commenting because the notion of alpha conversion always seems like an inflated idea in the lambda calculus context. Of course \x.x means the same thing as \y.y, no need to make a song and dance about it... Edit: to add a bit of value, here's Andrew Pitts on the subject: "The tedious and error-prone nature of ad hoc solutions to this semantically trivial, but pragmatically non-trivial issue of α-equivalence is widely acknowledged" https://www.cl.cam.ac.uk/~amp12/research/freshml/freshml-final-report.pdf https://www.cl.cam.ac.uk/~amp12/research/freshml/freshml-fin... (He is talking about programming language support for actually doing metaprogramming jobs that involve preserving alpha equivalence.)