Already since the dawn of mutation testing, equivalent mutants have been a subject of academic research. Up until now, all the investigated program analysis techniques (infeasible paths, trivial compiler equivalence, program slicing, symbolic execution) focussed on shielding the test engineer from the decision whether a mutant is equivalent or not. This paper argues for a complementary viewpoint: providing test engineers with powerful analysis tools (namely deductive verification) which show why a mutant is equivalent, or come up with a counter example if not. We illustrate by means of a series of increasingly challenging examples how such an approach provides valuable insights to the test engineer, as such paving the way for an actionable improvement of the test suite under analysis.