prove semantics_frees_exists

this subsumes typeset_tyvars_typeset_exists, since it's now a mutual
induction, and should solve the problems previously encountered with the
new more correct semantics. here's hoping there aren't any more.