another semantics tweak, and attempt to prove

typeset_tyvars_typeset_exists, but it fails on the abstraction case