start on adding implode/explode operations for strings

added characters and implode/explode to the AST, opsem, and typesys.
get semantics/proofs to build.
termination for v_to_char_list_def
get typeSysPropsTheory building
get metatheory building
get inferencer proofs building, fixes along the way
turn back on lem warnings, remove some unused variables

the warnings are useful (at least in my code) to see where things are
unimplemented or otherwise going awry.
add compilation of implode, explode, and char literals

to the toIntLang and toBytecode compilers. proofs (and intermediate
language semantics) not updated.
start updating semantics of intermediate langs, and proofs
get intLangExtra and patLangProof working
start updating bytecodeProof

prove ImplodeCode_correct
prove ExplodeCode_correct
update bytecodeProofTheory
more compiler proof fixes
finish updating compiler proofs
get initCompEnvTheory building
update repl proofs
get REPL translation working

that annoying op_apply theorem caught me again :(
Merge remote-tracking branch 'origin/master' into char
get bootstrap building
translation of characters