@Article{Vestergaard-Brotherston:03, author = "Ren{\'e} Vestergaard and James Brotherston", title = "A formalised first-order confluence proof for the $\lambda$-calculus using one-sorted variable names", journal = "Information \& Computation", volume = 183, number = 2, pages = "212--244", year = 2003 }