PrintForm
Definitions
finite
sets
Sections
AutomataTheory
Doc
At:
auto2
list
ind
1
2
1
1.
Alph:
Type
2.
P:
Alph*
Prop
3.
n:
. (
l:Alph*. ||l|| < n
P(l))
(
l:Alph*. ||l|| = n
P(l))
4.
l:
Alph*
0
||l||+1
By:
Inst
Thm*
l:A*. ||l||
0 [Alph;l]
Generated subgoals:
None
About:
Prop
n:
. (l:Alph*. ||l|| < n 
P(l)) (l:Alph*. ||l|| = n P(l))
0
||l||+1l:A*. ||l||
0
[Alph;l]
