PrintForm Definitions finite sets Sections AutomataTheory Doc

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

l:Alph*. ||l|| < n P(l)
By:
Thin 3
THEN
UnivCD
Generated subgoal:

13. 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
P(l)

About:
alllistimpliesless_thanapplyuniverse
functionpropintnatural_numbersubtractequal