PrintForm Definitions finite sets Sections AutomataTheory Doc

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

l:Alph*. ||l|| < n P(l)
By: Witness3 n-1
Generated subgoal:

13. 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)

About:
alllistimpliesless_thanapplysubtract
natural_numberuniversefunctionpropequalint