make term_ok_term_to_deep more robust

it could have generalised tmsig in the var case unnecessarily
improve termsem_cert

the tactic proof in the LAMB case is still ugly and not known to always
work
work on build_interpretation, esp. base case