tweak some broken proofs in hol_verificationScript.sml

it now builds