Thms nfa 1 Sections AutomataTheory Doc

NDA_act Def n == 1of(n)

Thm* Alph,States:Type, n:NDA(Alph;States). n StatesAlphStatesProp

pi1 Def 1of(t) == t.1

Thm* A:Type, B:(AType), p:a:AB(a). 1of(p) A

About:
!abstractionspreadalluniversefunctionproductmemberprop