Some prover progress.
Some prover progress.
Some serious rearchitecting of the new prover.  Implication rule is working up to the point of highlighting bound antecedents.
Can now apply implication theorems by clicking.  Bug present related to implication theorem like i = j and i <= k.
Implication bug resolved.  Added new proof step: expression matching theorem to true.  Basic integration with interactive prover.
Visual proving working, VC forward and back.  Implementing multi-application still to go.
Fixed a bug in the type system that caused a null pointer exception when reasoning about Entity.  Added a couple more proof rules.  Obvious_Flip_Realiz, Do_Nothing_Realiz, and Iterative_Append_Realize can all be proved interactively now.
Some optimizations after profiling the prover.
Bunch of work, I don't even.
Boom. Proving Obvious_Flip_Realiz.
Merge pull request #19 from hamptonsmith/proverWork

New prover is now in place.