(8steps)
PrintForm
Definitions
list
3
jlc
Sections
Support(jlc)
Doc
At:
list
length
wf
int
1
1.
T:
Type
|
|
(T List)
By:
Repeat (Unfolds [`list_length`;`letrec`;`letrec_body`;`letrec_arg`] 0)
Generated subgoal:
1
Y(
l,L. Case of L; nil
0 ; h.t
1+l(t))
(T List)
About:
(8steps)
PrintForm
Definitions
list
3
jlc
Sections
Support(jlc)
Doc
Y(
l,L. Case of L; nil 
0 ; h.t 1+l(t)) 
(T List)
|
| (T List)
Y(l,L. Case of L; nil 0 ; h.t 1+l(t)) (T List)
