Function derive_native_recursors_poly 

pub fn derive_native_recursors_poly(
    ctx: &Context,
    decl: &NestedDecl,
    num_params: usize,
    levels: &[String],
) -> KernelResult<Vec<NativeRecursor>>

derive_native_recursors_with_params for a universe-polymorphic family. Each restored recursor’s levels are its motive universes followed by the family’s own levels, in order.