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

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))

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

By: RWH YUnrollC 0 THEN Reduce 0

Generated subgoal:

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

About: