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.