Made the type checker explicitly test the body of a lambda expression against type theorems.  Fixed a bug were the last, rather than first, concrete type was saved for implicit type parameters.
Various progress and a new existential instantiation step (that doesn't quite work.)
Expanded the flexibility of the SubstituteInPlaceInAntecedent transformation to handle an 'and' on either side of the substitution more gracefully.  Added a timeout to the prover.  Added a preliminary ExistentialInstantiation transformation.
Merge pull request #50 from hamptonsmith/facilities3

General prover progress and timeouts.