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 and put under the exported universe parameter names).

Runs the nested-aware derivation (specialize → derive → restore), pairs each re-derived recursor with the exported one that carries the name Lean’s kernel gives it (nested_recursor_name: T.rec for a type of the declaration, <first type>.rec_<k> for the k-th auxiliary type), renames the re-derived recursors to those names (so self-references align), then requires every exported recursor to be the re-derived one of its name (recursor_matches: the same as written, or type-checked against the derived family and then definitionally equal — never compared by definitional equality unchecked). A missing pair or a recursor that is not the derived one is a rejection, and none is accepted under another recursor’s name. No exported recursor is ever installed: the family this returns is the kernel’s, and its rules call one another by the names it was renamed to. It is added with super::installed::add_derived_family, whose guard holds every name a term of the family mentions to the constants the install leaves in the environment.

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.