move EqualityType stuff into ml_repl_moduleTheory

the idea is that ml_repl_moduleTheory produces a theorem about the
module that is actually useful, i.e. without all the unnecessary
assumptions. side-bonus: can also define INPUT_TYPE and OUTPUT_TYPE at
this stage, and simplify the theorem with them.

also, put some comments in bootstrap_lemmasScript.sml about other things
that might deserve to be moved elsewhere.