Function normalize_binders 

pub fn normalize_binders(expr: &Expr, n: usize) -> Expr

Normalize only up to n binders deep.

This is useful for inspecting the head of a term without fully normalizing the bodies of lambdas/pis.