Suggested theorem prover features:
- Simple tactic to specify a list of possibly relevant proofs and search from a term to the goal - example usecase: group / ring / field arithmetic simplification
- Better inference on "replace" usage (this didn't seem to work in cases when unification ought to have been unambiguous)