Function elaborate_in 

pub fn elaborate_in(
    ctx: &Context,
    mctx: &mut MetaCtx,
    lctx: &[(String, Term)],
    term: &Term,
    expected: Option<&Term>,
) -> KernelResult<(Term, Term)>

Like elaborate but under a LOCAL CONTEXT lctx of bound variables. ctx is the kernel context already EXTENDED with those same variables (so infer_type sees them at the leaves), while lctx is the parallel (name, type) list the unifier uses for higher-order PATTERN unification. Descending under a λ extends both — which is how a metavariable applied to a bound variable (a motive ?P n) gets solved in a body.