tweak to example6 for better interactive use
possible fix in termsem_cert

weird issue to do with wf_to_inner_mk_to_inner's approach and the
pervasive type instantiation (vti) not quite matching up. solved by
ignoring the former and using a custom tactic instead.
use _ instead of ' for tyvar variants

to avoid warnings about non-standard vartypes