Function eliminate_nested 

pub fn eliminate_nested(
    ctx: &Context,
    block: &NestedBlock<'_>,
) -> KernelResult<Elimination>

Reduce a nested block to an ordinary mutual block exactly as Lean’s kernel does (elim_nested_inductive).

Every constructor field of every member is scanned left to right, top-down. A fully applied inductive C A₁ … Aₚ i₁ … iᵣ that is not a member, whose PARAMETERS mention a member, is a nested occurrence: it becomes an auxiliary family Aux P i₁ … iᵣ over the block’s parameters, one per distinct C A₁ … Aₚ, whose constructors are C’s constructors at A₁ … Aₚ rewritten the same way. Auxiliary families join the end of the queue, so the block order — and with it the recursors, motives and minor premises — is Lean’s (all source members first, then each auxiliary as it is discovered: List (Prod α T) before the Prod α T inside it). Indices stay indices: an indexed container becomes an indexed auxiliary family. A nested occurrence whose parameters mention a constructor’s own field binders is an invalid declaration, as Lean says; one whose indices mention the block is declined. Nothing here is trusted: the caller registers the block through the trusted mutual door, which checks positivity and universes.