(7steps total)
PrintForm
Definitions
list
1
Sections
StandardLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
reduce
wf
1
1.
A
: Type
2.
B
: Type
3.
f
:
A
B
B
4.
k
:
B
5.
as
:
A
List
reduce(
f
;
k
;
as
)
B
By:
ListInd 5
Generated subgoals:
1
reduce(
f
;
k
;nil)
B
1
step
2
6.
u
:
A
7.
v
:
A
List
8. reduce(
f
;
k
;
v
)
B
reduce(
f
;
k
;
u
.
v
)
B
4
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(7steps total)
PrintForm
Definitions
list
1
Sections
StandardLIB
Doc
B
reduce(f;k;as) 
B
