Nuprl - Pf auto2_list

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:

l:Alph*. ||l|| < n P(l)

By: NatInd 5

Generated subgoals:

1 l:Alph*. ||l|| < 0 P(l)

2 5. n:
6. 0 < n
7. l:Alph*. ||l|| < n-1 P(l)
l:Alph*. ||l|| < n P(l)

About:

1	`l:Alph*. \|\|l\|\| < 0 P(l)`
2	5. `n:` 6. `0 < n` 7. `l:Alph. \|\|l\|\| < n-1 P(l)` `l:Alph. \|\|l\|\| < n P(l)`