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*

P(l)

By: Assert (n:, l:Alph*. ||l|| < n P(l))

Generated subgoals:

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

2 5. n:, l:Alph*. ||l|| < n P(l)
P(l)

About:

1	`n:, l:Alph*. \|\|l\|\| < n P(l)`
2	5. `n:, l:Alph*. \|\|l\|\| < n P(l)` `P(l)`