Function bind_self_recursion 

pub fn bind_self_recursion(name: &str, body: &Term) -> Term

Replace every Global(name) by Var(name) (turning a free type-variable reference into a reference to the binder this pass prepends). Recursive-definition sugar: if body refers to the definition’s own name as a free Global, bind that self-reference with a fix so the definition can call itself — Definition f : T := … f … . becomes f := fix f. …. The kernel’s termination guard (run by infer_type) then certifies the recursion decreases structurally; a body with no self-reference (or one that already wrote an explicit fix, whose self-references are already bound Vars) is returned unchanged. A self-reference SHADOWS any same-named global, so a recursive Definition add over Nat overrides a built-in add.