PrintForm Definitions finite sets Sections AutomataTheory Doc

At: auto2 list ind 1 1 1 2 1 1 1
1. Alph: Type
2. P: Alph*Prop
3. n:
4. 0 < n
5. l:Alph*. ||l|| < n-1 P(l)
6. (l:Alph*. ||l|| < n-1 P(l)) (l:Alph*. ||l|| = n-1 P(l))
7. l: Alph*
8. ||l|| < n
9. ||l|| < n-1

P(l)
By: Witness5 l
Generated subgoal:

15. (l:Alph*. ||l|| < n-1 P(l)) (l:Alph*. ||l|| = n-1 P(l))
6. l: Alph*
7. ||l|| < n
8. ||l|| < n-1
9. ||l|| < n-1 P(l)
P(l)

About:
applyuniversefunctionlistpropint
less_thannatural_numberallimpliessubtractequal