SeLFiE: make the caching mechanism for dive-in constructs modifier-sensitive?

[yutakang]

The current implementation assumes that modifiers (arguments to the induction tactic) are not used in any inner assertions.
This is often true, and I do not see any concrete use case where I want to refer to modifiers within inner assertions.
But such cases are not explicitly banned.

I should either

• ban such cases,
• or modify the caching mechanism.

[yutakang]

It is mostly about Eval_Unary.ML