Michael Norrish. Mechanising lambda-calculus using a classical first order theory of terms with permutations. Higher-Order and Symbolic Computation, 19(2-3):169-195, 2006. [doi]
@article{Norrish06, title = {Mechanising lambda-calculus using a classical first order theory of terms with permutations}, author = {Michael Norrish}, year = {2006}, doi = {10.1007/s10990-006-8745-7}, url = {http://dx.doi.org/10.1007/s10990-006-8745-7}, researchr = {https://researchr.org/publication/Norrish06}, cites = {0}, citedby = {0}, journal = {Higher-Order and Symbolic Computation}, volume = {19}, number = {2-3}, pages = {169-195}, }