(5steps total)
Gloss
PrintForm
Definitions
NuprlPrimitives
Sections
NuprlLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
sfa
doc
type
poly
identity
1
1
1.
f
:
D
:Type.
D
D
2.
A
: Type
3.
a
:
A
4.
f
{
a
:
A
}
{
a
:
A
}
f
(
a
) =
a
A
By:
BackThru:
z
:{
a
:
A
}.
z
=
a
A
Generated subgoals:
1
5.
z
: {
a
:
A
}
z
=
a
A
1
step
2
a
{
a
:
A
}
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(5steps total)
Gloss
PrintForm
Definitions
NuprlPrimitives
Sections
NuprlLIB
Doc
D:Type. D
D
{a:A}
f(a) = a 
z:{a:A}. z = a 
