@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
}