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