We start by describing how higher-order function support can be added to a (first order) functional verification framework. We cover both the higher-order construct management and framework extensions necessary for constraint specification. Next, we outline a termination proof constructor for the aforementioned framework. In order to provide effectiveness as well as performance, our approach combines different techniques in a weeding-out strategy where each partial proof is carried on to the next prover. To enable high-level reasoning about formulas during termination proofs, we make use of the underlying verification framework while maintaining soundness by carefully restricting the acceptable formula space. Finally, we propose an extension to the framework input language that adds support for generic type polymorphism while maintaining compatibility with legacy features.