Function desugar_hoas 

pub fn desugar_hoas(node: Node) -> Node

Higher-order abstract syntax (issue #51, D7): rewrite the surface keyword forall to the kernel binder Pi. Both forms share identical structure (<binder> (Type x) body), so the desugarer walks the AST and rewrites the head leaf in place. Object-language binders are encoded as host-language lambda and Pi/forall, letting substitution and capture-avoidance reuse the kernel primitives without a separate object-level binder representation.