refactor prover to add elaborate; fix performance in undoing binds