Function derive_below 

pub fn derive_below(ctx: &Context, ind: &str) -> KernelResult<(Term, Term)>

I_below : Π(A…). Π(motive : I A… → Type 0). I A… → Type 0

The course-of-values PACKAGE: below motive t is the type of “a motive value for every subterm reachable below t”, right-nested one entry per recursive field and closed with Unit:

below motive (C x⃗) ⤳ Prod (Prod (motive xⱼ) (below motive xⱼ)) (… Unit)   -- recursive fields only

Each entry is EXACTLY the type of brecOn’s internal aux xⱼ, which is what makes derive_brec_on’s payload the recursive results themselves rather than a repacking. A strictly-positive FUNCTIONAL field xⱼ : Π(z:B…). I A… contributes Π(z:B…). Prod (motive (xⱼ z…)) (below motive (xⱼ z…)), as in Acc.

Lean’s is Sort (max 1 u)-valued over PProd/PUnit; ours uses the prelude’s Prod/Unit and is therefore pinned to Type 0, the sort those live at.