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.
Fixed an error that caused binders to fail to bind to lambda expressions.
Commiting a veresion that might be broken.
Fixed an error that caused expressions containing top-level conjuncts to be entered into the prover model as a single conjunct rather than being split up.
Added a step to eliminate redundant conjuncts during theory development.
Merge pull request #51 from hamptonsmith/facilities3

Various prover improvements.
Some reformatting.
Added a summary section to the proof output file, along with some metrics about each VC proof.
Merge pull request #52 from hamptonsmith/facilities3

Facilities3
Fixed a bug in GeneralApplication that caused prerequisite theorems to not include the theorem that spawn the step, hosing proof output.  Fixed a bug in MainProofLevel that caused cycle detection to fail when multiple cycles were encountered.  Added a defensive check to removeConsequent in PerVCProver.  Fixed a bug in ExpandAntecedentBySubstitution that caused equality theorems to become symmetrical and then make meaningless changes.  Fixed an error in MTType that allowed equals() to go into an infinite recursive loop.
Merge pull request #53 from hamptonsmith/facilities3

Fixed a bug in GeneralApplication that caused prerequisite theorems to n...
Added flags in AutomatedProver to permit a number of heuristics to be toggled on or off.  Added a new step to the automated prover that occasionally prunes out 'obvious' antecedents like 'true' or 'S = S'.
Merge pull request #54 from hamptonsmith/facilities3

Added flags in AutomatedProver to permit a number of heuristics to be to...