Nuprl - Pf list length wf nat 1 1 1 1 2 1

(13steps) PrintForm Definitions list 3 jlc Sections Support(jlc) Doc

1. T: Type
2. L: T List
3. u: T
4. v: T List
5. (Case of v; nil 0 ; h.t 1+Y((l,L. Case of L; nil 0 ; h.t 1+l(t)),t))
6. h: T
7. t: T List
8.

Y((l,L. Case of L; nil 0 ; h.t 1+l(t)),t)

By: RWH YUnrollC 0 THEN ListInd -2 THEN Reduce 0

Generated subgoals:

1 0

2 9. u1: T
10. v1: T List
11. (l,L. Case of L; nil 0 ; h.t 1+l(t))(Y(l,L. Case of L; nil 0 ; h.t 1+l(t)),v1)
1+Y((l,L. Case of L; nil 0 ; h.t 1+l(t)),v1)

About:

(13steps) PrintForm Definitions list 3 jlc Sections Support(jlc) Doc

1	`0`
2	9. `u1:` `T` 10. `v1:` `T List` 11. `(l,L. Case of L; nil 0 ; h.t 1+l(t))(Y(l,L. Case of L; nil 0 ; h.t 1+l(t)),v1)` `1+Y((l,L. Case of L; nil 0 ; h.t 1+l(t)),v1)`