(5steps total)
PrintForm
Definitions
NuprlPrimitives
Sections
NuprlLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
sfa
doc
void
via
isect
1
1
1.
X
:
A
:Type.
A
2.
X
(
A
:Type.
A
)
X
Void
By:
Witness2: {0:
} THEN Witness2: {1:
}
Generated subgoal:
1
3.
X
{0:
}
4.
X
{1:
}
X
Void
2
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(5steps total)
PrintForm
Definitions
NuprlPrimitives
Sections
NuprlLIB
Doc
A:Type. A
(A:Type. A)
X VoidA:Type. A
(A:Type. A)
X Void
} THEN Witness2: {1:} {0:}
{1:}
X Void
