prove many of the cheats in exhLangProofScript.sml

remaining ones are all about correctness of pmatch_exh

match_exists_tac showing its usefulness in places here