fix: `grind` normalizes the goal before negating it

`grind` now normalizes the goal before applying `byContra`. An implication or universal quantifier exposed by a `[grind norm]` rule or a reducible definition is then introduced like a syntactic one, instead of being negated together with the rest of the goal. This fixes the `Imp` example reported by Sebastian Graf after #15378.

The normalizer also no longer distributes a non-dependent implication over a conjunction: `p → a ∧ b` is kept, since `grind` obtains `a ∧ b` from `p` by propagation and the split only duplicates the antecedent. `Grind.forall_and` still applies to any binder telescope with at least one dependent binder, such as `∀ x, p x → q x ∧ r x` or `∀ x y, s x y → q x ∧ r y`, so each conjunct keeps its own E-matching pattern. Both simp engines instantiate binders with fresh variables, and the `Sym` engine simplifies a whole telescope as one unit, so the decision is made at the outermost binder by `forallImpAnd?`, which walks the telescope and builds the proof with `forall_congr` and `implies_congr_right`.

`mkEqTransCore` and `mkEqTransCoreProp` are added to `AppBuilder`, and `mkEqTrans` uses the former.

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