(7steps total)
PrintForm
Definitions
hol
list
1
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
it
sum
wf
1
1.
l
:
List
it_sum(
l
)
By:
ListInd 1 THEN CAuto
Generated subgoals:
1
it_sum(nil)
1
step
2
0
it_sum(nil)
1
step
3
2.
u
:
3.
v
:
List
4. it_sum(
v
)
it_sum(cons(
u
;
v
))
2
steps
4
2.
u
:
3.
v
:
List
4. it_sum(
v
)
0
it_sum(cons(
u
;
v
))
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(7steps total)
PrintForm
Definitions
hol
list
1
Sections
HOLlib
Doc
List
it_sum(l) 
List
it_sum(l) it_sum(nil) 
0
it_sum(nil)
List
it_sum(cons(u; v))
List
0it_sum(cons(u; v))
