@PhdThesis{T2,
  key    =       {T2},
  author = 	 {Christoph Benzm\"uller},
  title = 	 {Equality and Extensionality in Higher-Order Theorem Proving},
  school = 	 {Naturwissenschaftlich-Technische Fakult{\"a}t I, Saarland University, Saarbr{\"u}cken, Germany},
  year = 	 1999,
  pages =        {1--174},
  CHRISNOTE =	 {T2},
  URL =		 {www.ags.uni-sb.de/~chris/papers/T2.pdf}
}