(5steps total)
Gloss
PrintForm
NuprlPrimitives
Sections
NuprlLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
sfa
doc
type
poly
constant
T
:Type,
f
:(
D
:Type.
D
T
),
A
:Type,
a
:
A
,
B
:Type,
b
:
B
.
f
(
a
) =
f
(
b
)
T
By:
Auto
Generated subgoal:
1
1.
T
: Type
2.
f
:
D
:Type.
D
T
3.
A
: Type
4.
a
:
A
5.
B
: Type
6.
b
:
B
f
(
a
) =
f
(
b
)
T
4
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(5steps total)
Gloss
PrintForm
NuprlPrimitives
Sections
NuprlLIB
Doc
T:Type, f:(
D:Type. D
T), A:Type, a:A, B:Type, b:B. f(a) = f(b) 
T
