Thm* Alph,States:Type, a:Automata(Alph;States). a StatesAlphStates
Thm* A:Type, B:(AType), p:a:AB(a). 1of(p) A
About: