Make @prover implementation easier w.r.t. auto_simplify and replacements

[wwitzel]

trafficstars

Currently, one needs to 'preserve_all' for all but the last step and this can get tricky. It would be slightly less efficient but easier to handle auto_simplify and replacements in the wrapper after the first pass by re-running the last instantiation. Not sure how to handle it if the last step is modus ponens, generalization, or deduction, but there should be a way to do this.