consolidating some iteration functions.
a first sketch of AutoRewrite.

- There should be a lot of opportunities for reuse with AutoProver
  but the current abstractions are not great.