Nuprl - Pf lang_prod

1. Alph: Type
2. L: Alph*Prop
3. l: Alph*

(i:{0...||l||}. L(l[0..i]) & null(l[i..||l||])) L(l)

By: Analyze 0 THEN Analyze 0

Generated subgoals:

1 4. i:{0...||l||}. L(l[0..i]) & null(l[i..||l||])
L(l)

2 4. L(l)
i:{0...||l||}. L(l[0..i]) & null(l[i..||l||])

About:

1	4. `i:{0...\|\|l\|\|}. L(l[0..i]) & null(l[i..\|\|l\|\|])` `L(l)`
2	4. `L(l)` `i:{0...\|\|l\|\|}. L(l[0..i]) & null(l[i..\|\|l\|\|])`