(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
2
1.
A
: Type
2.
B
: Type
3.
f
:
A
B
B
4.
k
:
B
5.
A
List
6.
u
:
A
7.
v
:
A
List
8. reduce(
f
;
k
;
v
)
B
reduce(
f
;
k
;
u
.
v
)
B
By:
RecUnfold `reduce` 0 THEN AbReduce 0
Generated subgoal:
1
f
(
u
,reduce(
f
;
k
;
v
))
B
3
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
B
reduce(f;k;u.v) 
