chore: type check the declarations produced by nested inductive restoration

This PR makes the kernel recheck the declarations it adds to the environment after
eliminating a nested inductive type.

These checks are redundant, but they serve as sanity checks and may prevent soundness bugs
if the nested-inductive code is still missing any required validations.