Def NDA(Alph;States) == (StatesAlphStatesProp)States(States)

Thm* Alph,States:Type{i}. nd_automata{i}(Alph;States) Type{i'}