fix: decide inductive predicates up to universe normalization

This PR makes the inductive checker test a resulting universe for zero up to normalization,
so that `Sort (imax 1 0)` and `Sort 0` describe the same inductive type.
The two spellings previously disagreed on whether a constructor field may carry data,
on whether the recursor eliminates only into `Prop`, and on whether the type is a K-like
reduction target. Only declarations produced with metaprogramming are affected,
since the elaborator normalizes levels before the kernel sees them.

`nanoda` decides all three semantically, so it and the kernel disagreed on these declarations.
It derives recursors and checks them against the export rather than trusting it,
so a disagreement about the elimination level makes it reject an export the kernel accepted.

This widens what the kernel accepts, but it is not a soundness fix: the syntactic tests
all erred in the restrictive direction, rejecting declarations that are in fact sound.