Suggestion: clear unused assumptions first

[QinshiWang]

It will be helpful if the tactic generated by hammer can first remove unused assumptions. In my simple example, (a) takes 0.046s while (b) takes 5.888s.

(a)
clear -H13.
Time hauto use: Z.add_0_r unfold: sval_refine.
(b)
Time hauto use: Z.add_0_r unfold: sval_refine.

It's worth mentioning that I added clear -H13 at the beginning because otherwise hammer would time out. But that doesn't matter for the main point.

[lukaszcz]

This shouldn't be too hard. I'll do it sometime in the future, in several months perhaps.

[QinshiWang]

That'll be great!