feat: type-check generated recursors in the kernel (#14808)

This PR adds a new defensive check to the kernel.

**TL;DR.** When the kernel generates a recursor for an inductive type,
it installs the recursor and its computation rules with `add_core`,
which does not re-check them. This PR adds a verification pass that (1)
type-checks each generated recursor's type and (2) checks that each
computation rule is type-preserving: reducing the recursor applied to a
constructor yields a term whose type is the recursor's declared result
type. This catches a recursor whose minor-premise type and reduction
rule disagree, for example a minor premise that expects an induction
hypothesis while the rule omits it. Checking only that a rule's
right-hand side has some type is not enough, because an under-applied
minor premise is still a well-typed (function) term. The check is
defense-in-depth: it does not change what the kernel accepts for
well-formed inductives, and only rejects declarations that were already
malformed.

When the kernel adds an inductive type, it generates the recursor's type
and its computation rules and installs them with `add_core`, which does
not re-check them. The surrounding machinery is trusted to produce a
consistent recursor. This PR re-verifies that output.

The check has two parts. First, the recursor's type is type-checked.
Second, for each constructor, the recursor applied to that constructor
is reduced by one step and the type of the reduct is compared against
the type of the un-reduced application; the two must be definitionally
equal. The second part is what separates a type-preserving rule from a
merely well-typed right-hand side: if a minor premise's type expects an
induction hypothesis that the rule does not supply, the reduct is an
under-applied minor premise. That reduct still has a type, but a
function type rather than the recursor's result type, so the check
fails.