@TechReport{harper+:lf-theory-tr,
  author = 	 {Robert Harper and Frank Pfenning},
  title = 	 {On Equivalence and Canonical forms in the LF Type Theory},
  institution =  {Carnegie Mellon University Computer Science Department},
  year = 	 2000,
  number =	 {CMU--CS--00--148},
  address =	 {Pittsburgh, PA},
  month =	 {July}
}