This module contains functions for converting mutually recursive functions with constant arguments by moving the constant arguments into a Section sentence.

A Section sentence must be used in case of higher-order functions to tell Coq that the function does not change. Otherwise Coq cannot determine that functions using higher order functions terminate in some cases.