minor fixes to broken proofs about compile_prog

must have been broken by some recent changes to HOL?
fix proof in holAxiomsSyntaxTheory

I believe this is (more) fallout from commit 875ba111 in HOL.
additions to cakeml_compset for compiling datatype defs
add some cakeml_compset things for structure declarations
translator now knows about modules
translator can now translate into a module
clean up some of the code
derive thm about generated module, demo file
HOL Light example works again
Merge remote-tracking branch 'origin/master' into conLang_wip
tweaks to the translator's module exporter
HOL Light kernel now translates into a module
mini/std prelude put in Lib files in prep for repl_step trans
Merge remote-tracking branch 'origin/master' into conLang_wip