prove consistency for the stateful system
make term_ok and type_ok imply good_defs
prove two of the cheats in hol_verificationScript.sml