@TechReport{	  abelCoquandNorell:lfprop,
  author	= {Andreas Abel and Thierry Coquand and Ulf Norell},
  title		= {Connecting a Logical Framework to a First-Order Logic
		  Prover (Extended Version)},
  institution	= {Department of Computer Science, Chalmers University of
		  Technology},
  year		= 2005,
  address	= {Gothenburg, Sweden},
  note		= {Available under
		  http://www.cs.chalmers.se/\~{}ulfn/papers/fol.html}
}