rough and ready induction

nicer error message, indicating which type is empty (relying on metatheoretical completeness proof here)

observe context more carefully when producing "fresh" variables -- for increased chances that method "subst" works in local context (including that of forked proofs);