add support for lambdas in TPTP THF generator + killed an unsound type encoding (because the monotonicity calculus assumes first-order)
added generation of lambdas in THF
improved translation of lambdas in THF
added choice operator output for
improved handling of induction rules in Sledgehammer
added generation of induction rules
removed explicit reliance on Hilbert_Choice.Eps