Remove Q.prove in ml_monad_translator_interfaceLib

[ordinarymath]

As in title. Right now loading that Library is extremely slow.

[oddgarden6465]

Hello! I would like to work on this issue, can you give me some instructions?

[ordinarymath]

Hi do you have experience with HOL. This issue is about removing top level uses of Q.prove in a https://github.com/CakeML/cakeml/blob/master/translator/monadic/ml_monad_translator_interfaceLib.sml and moving them to https://github.com/CakeML/cakeml/blob/master/translator/monadic/ml_monad_translatorScript.sml.

Here's an example of a top_level Q.prove
https://github.com/CakeML/cakeml/blob/43b8014f368073c1b7bf32d38bae36ea9e04ad63/translator/monadic/ml_monad_translator_interfaceLib.sml#L533C1-L538C1

This is in a function and not a top level Q.prove
https://github.com/CakeML/cakeml/blob/43b8014f368073c1b7bf32d38bae36ea9e04ad63/translator/monadic/ml_monad_translator_interfaceLib.sml#L365C1-L368C6

[tanyongkiam]

Closed by #1484