(3steps total)
PrintForm
NuprlPrimitives
Sections
NuprlLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
sfa
doc
void
rectype
1
1.
X
: rec(
A
.
A
)
X
Void
By:
RecTypeInd Hyp:-1
Generated subgoal:
1
1.
Q
: rec(
A
.
A
)
Prop
2.
X
:{
X
:rec(
A
.
A
)|
Q
(
X
) }.
X
Void
3.
X
: {
X
:rec(
A
.
A
)|
Q
(
X
) }
X
Void
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(3steps total)
PrintForm
NuprlPrimitives
Sections
NuprlLIB
Doc