make mlstring_case_conv slightly more robust/lenient

attempt to prove that the lhs of the generated theorem is equal to the
input term, rather than just failing if it isn't aconv
add better mlstring_CASE handling to translator

also had to use the classic pmatch heuristic to define TRANS and MK_COMB
in the HOL Light kernel because the default heuristic makes a case
expression that is too complicated for my mlstring_case_conv to deal
with