Letfuns shouldn't have to live in the same module #13
Description
Currently payloadLang$config contains a field letModule, and the assumption made for payload_to_cakeml is that all functions used in Let bindings live in a module with name letModule.
This seems overly restrictive: for example, it would be convenient to be able to supply some functions as part of a standard library.
This issue is to adapt the payload_cakeml phase and the associated proofs to allow the letfuns to live in different modules.