So what you are saying is that when you find out that some assumption that you asserted was actually wrong, you'd like to know where it was used in the proof.
We advise users to thoroughly model check their specifications before embarking on any proof. In our experience, using the model checker is a great way for validating a spec. (It could certainly detect the fallacy in the example that you give.) Doing so helps you avoid the problem in the first place.
Second, the proof system has an approximation for the functionality that you request: when you modify the assertion of some fact (or change a definition), you can relaunch the prover. Since all previous results of proof attempts are cached, steps that do not syntactically depend on the definition or fact will not be rechecked, and you quickly see which steps fail. Of course, if your assumption appears in a global USE, all steps will need to be reproved.
Stephan