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

At: list length wf nat 1 1 1 1 2 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))

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

By: GenConcl ((Case of v; nil 0 ; h.t 1+Y((l,L. Case of L; nil 0 ; h.t 1+l(t)),t)) = n)

Generated subgoal:

16. n:
7. (Case of v; nil 0 ; h.t 1+Y((l,L. Case of L; nil 0 ; h.t 1+l(t)),t)) = n
01+n

About:
listlist_ind
natural_numberaddlambdaapplyycombuniverseequalmember

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