Substitutions for Lambda-Free Higher-Order Terms

This theory provides a formalization of substitutions on \(\lambda\)-free higher-order terms, establishing a structured framework with the expected algebraic properties. It introduces a type construction for the rigorous definition and manipulation of substitutions. The main theorem of this theory proves the existence of fixed-point substitutions under acyclicity, a theorem that is too often regarded as trivial in the literature.