Add dt lemma: zero size implies nullary constructor.
Fix assertion.