better support for translating recursion through higher-order functions

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