(8steps)
PrintForm
list
3
jlc
Sections
Support(jlc)
Doc
At:
list
length
wf
int
1
1
1.
T:
Type
Y(
l,L. Case of L; nil
0 ; h.t
1+l(t))
(T List)
By:
RWH YUnrollC 0
THEN
Reduce 0
Generated subgoal:
1
(
L.Case of L; nil
0 ; h.t
1+Y((
l,L. Case of L; nil
0 ; h.t
1+l(t)),t))
(T List)
About:
(8steps)
PrintForm
list
3
jlc
Sections
Support(jlc)
Doc