fix: keep case-splits needed to replay `grind?` scripts

This PR fixes `grind?` and `finish?` dropping case-splits from their generated scripts when the proof does not use the case-split, but the rest of the script does. For example, a case-split may introduce a term that E-matching uses later. The scripts then failed to replay, and `grind?` dropped theorems from its `grind only` suggestions.

When generating a script, non-chronological backtracking now drops a case-split only if the script still closes the goal without it. Otherwise, the case-split is kept and its remaining alternatives are explored. If they cannot be closed, the case-split is dropped as before.

Closes #16037

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>