NonTerminals (DTConUA (f,X)) = dom f by Th2;
hence DTConUA (f,X) is with_nonterminals by DTCONSTR:def 7; :: thesis: verum