feat: type-check generated recursors in the kernel

This PR adds a 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.