Def Automata(Alph;States) == (StatesAlphStates)States(States)

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