PrintForm Definitions nfa 1 Sections AutomataTheory Doc

At: nd compute list wf 1
1. Alph: Type
2. St: Type
3. NDA: NDA(Alph;St)
4. l: Alph*

q:St. NDA(l)q Prop
By: ListInd 4
Generated subgoals:

1 q:St. NDA(nil)q Prop
25. u: Alph
6. v: Alph*
7. q:St. NDA(v)q Prop
q:St. NDA(u.v)q Prop

About:
allmemberpropuniverselistnilcons