Function derive_brec_on 

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

I_brecOn : Π(A…). Π(motive : I A… → Type 0). Π(t : I A…). Π(F : Π(s). I_below A… motive s → motive s). motive t

Course-of-values RECURSION — the eliminator that hands the step function every subterm at once, which is how | n+2 => … (and halve/fib/pairSum) is a structural definition rather than a re-expressed mutual block. Built the way Lean builds it: one structural recursion producing the PAIR (motive s, below motive s), then the first projection.