Nuprl - Pf lang_sing

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

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

By: Reduce 0 THEN Analyze 0

Generated subgoals:

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

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

About:

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