tweak good_context_thm in termsem_cert so it matches the hyp
make examples 1 and 2 use termsem_cert rather than build_interpretation