Function substitute 

pub fn substitute(body: &Term, var: &str, replacement: &Term) -> Term

Substitute a term for a variable: body[var := replacement].

Performs capture-avoiding substitution. Variables bound by lambda, pi, or fix that shadow var are not substituted into.

Capture Avoidance

Given substitute(λx. y, "y", x), the result is λx. x (not λx. x with the inner x captured). This implementation relies on unique variable names from parsing.

Term Forms

• Sort, Lit, Hole, Global - Unchanged (no variables)
• Var(name) - Replaced if name == var, unchanged otherwise
• Pi, Lambda, Fix - Substitute in components, respecting shadowing
• App, Match - Substitute recursively in all subterms