Function verify_nested_bundle 

pub fn verify_nested_bundle(
    env: &Environment,
    lparams: &[Name],
    num_params: u32,
    specs: &[InductiveSpec],
    exported_recs: &[RecursorVal],
) -> Result<DerivedFamily, KernelError>

Verify a nested inductive bundle for export replay and return the kernel-derived family to install (recursors renamed to the exported names).

Runs the nested-aware derivation (specialize → derive → restore), pairs each re-derived recursor with an exported one by the set of constructors its rules fire on, renames the re-derived recursors to the exported names (so self-references align), then requires every exported recursor to be definitionally equal to the corresponding re-derived one (recursor_matches). A missing pair or a failed def-eq is a rejection — no exported recursor is ever accepted without a sound kernel re-derivation.

Returns KernelError::UnsupportedNestedInductive for shapes this stage cannot un-nest (parametrized families, family in an index position, non-inductive or multi-member containers), which replay buckets as the named nested inductives unsupported feature — never a wrong accept.