use HOL_ERR rather than Fail
start working on termsem_cert