(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
dom
fun
degenerate
A
:Type. Void
A
=ext {
x
.
x
:Void
A
}
By:
Auto
Generated subgoals:
1
1.
A
: Type
2.
X
: Void
A
X
{
x
.
x
:Void
A
}
3
steps
2
1.
A
: Type
2.
X
: {
x
.
x
:Void
A
}
X
Void
A
1
step
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. Void
A =ext {
x.x:VoidA} A:Type. VoidA =ext {x.x:VoidA}A
X 
{x.x:VoidA}
x.x:VoidA}
X VoidA
