Nuprl - Pf list length wf int 1 1 1 1

(8steps) PrintForm list 3 jlc Sections Support(jlc) Doc

1. T: Type
2. L: T List

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

By: ListInd 2 THEN Reduce 0

Generated subgoals:

1 0

2 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))
1+Y((l,L. Case of L; nil 0 ; h.t 1+l(t)),v)

About:

(8steps) PrintForm list 3 jlc Sections Support(jlc) Doc

1	`0`
2	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))` `1+Y((l,L. Case of L; nil 0 ; h.t 1+l(t)),v)`