some cleanup of AutoProver2.
a very simple "tactic language"

- the problem with a more sophisticated one
  is managing multiple contexts and a unified
  substitution.