better support for translating recursion through higher-order functions

[xrchz]

The translator works on recursive functions that recurse as an argument to MAP (and maybe some other simple functions), but in general recursion as an argument to a higher-order function makes the translator fail when attempting to prove the certificate theorem using the induction theorem. A solution to the problem will probably require a more general form of certificate theorems (in particular, allowing arbitrary preconditions on arguments).

See this thread: https://lists.cakeml.org/private/dev/2014-December/000662.html

[tanyongkiam]

It is currently done by manually inlining the closure to a higher-order function and translating that instead. A more general solution is desired but requires rethinking how the translator works.