fix: restore two `grind` behaviors lost with the `(∀ x, p x) → q` normal form

This PR fixes two `grind` regressions introduced by #15420 and reported in leanprover/cslib#1141, where proofs about inductive predicates over λ-terms that v4.35.0 proved fail on v4.36.0-rc1. The normalizer now rewrites `∀ _ : α, True` to `True` for every `α`, not only for propositions, and the eager `cases` that `grind` applies to new hypotheses resets the E-matching round counter like any other case split.

Both behaviors were side effects of the rule rewriting `(∀ x, p x) → q` into `(∃ x, ¬p x) ∨ q` that #15420 removed. First, the rule turned `(∀ t : α, True) → q` into `(∃ t, False) ∨ q`, that is `q`, while the `imp_true_eq` case of `simpForall` only fires when the antecedent is a proposition. Such antecedents arise from conditional equation theorems like `(∀ t, x = abs (abs t) → False) → f x = false` once `x` is instantiated with another constructor: the condition simplifies to `∀ t, True`, the implication becomes an opaque atom nothing can establish, and `f x = false` is lost. Both normalizers now use `implies_true`, which holds for any `Sort`. Second, when a universally quantified antecedent is refuted by propagation, the witness used to come from a 1-case split on the `∃` inside the disjunction, and `selectNextSplit?` resets the round counter after every split. Now `grind` asserts `∃ x, ¬p x` as a new fact and `applyCases?` eliminates it, so the same proof needed one more round within a single stretch. `applyCases?` now resets the counter in the subgoals it creates, since it performs a case split.

The `grind_list2` benchmark no longer needs the `ematch := 6` added in #15420. The failure state pinned in `grind_11081.lean` changes because the `(∀ t, True) → …` hypotheses are now simplified.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>