- Fix memory leak.  Proof.cleanup doesn't seem to work...
- Add automated proof support.  This can probably be done in a series
  of stages:
     1) Create a semi-automated prover that applies rules when it can
        and seeks user input when it has to (inherit from UserRuleSource).
     2) Progressively refine the rule heuristic until the
        semi-automated prover no longer needs human input.
     3) Rigorously test.
     4) Convert to pure automated prover.
- Finish commenting.

- Implement auto-prover strategy
   1 ) goal is to get all formulas on the lhs with the form VAR or ~VAR
   2 ) if rhs is VAR and rhs != any lhs(i) --> notR
   2a) if rhs is VAR = some lhs(i) --> hyp
   3 ) if rhs is & --> andR
   4 ) if rhs is ~X --> notR
   5 ) if rhs is ==> --> impR
   6 ) if rhs is X|~X or ~X|X --> magic
   7 ) if rhs is X|Y and lhs contains only ~(W|Z)'s, VAR's, and ~VAR's
          --> orR1, then orR2 if necessary
   8 ) if rhs is X|Y and lhs not described by 7's condition --> notR
   8 ) if rhs is constant (i.e. false)...
   8a) if lhs contains non-basic formulae only of form ~(X|Y) --> notL
   8b) if lhs contains X&Y --> andL
   8c) if lhs contains p and ~p --> notL on ~p
   8d) if lhs contains ~X where X is non-basic, non-OR --> notL
   8e) if lhs contains X==>Y, impL