[prove] fix hammer strategy & improve feedback

Fixes hammer strategy when applying tactics. Previously, when a CRC contains a tactic node, this transformation is always checked first. However, when the goal changes or the strategy is modified, perhaps this transformation is no more the first one that applies. This means that, once a tactic has been applied, we are stuck to it for this node forever.

The MR fixes this behavior: strategies are always tried in sequence from the configuration, and a Tactic CRC is only used when it corresponds to the newly applied tactic.