Nuprl - Pf list all 2 wf 1

1. T: Type
2. P: T
3. L: T List

xL.P(x)

By: ListInd 3 THEN Reduce 0

Generated subgoals:

1 true

2 4. u: T
5. v: T List
6. xv.P(x)
(P(u)xv.P(x))

About:

1	`true`
2	4. `u:` `T` 5. `v:` `T List` 6. `xv.P(x)` `(P(u)xv.P(x))`