(4steps total)
PrintForm
NuprlPrimitives
Sections
NuprlLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
sfa
doc
pairing
projs
1
1.
A
: Type
2.
B
:
A
Type
3.
p
:
u
:
A
B
(
u
)
p
= <
p
.1,
p
.2>
a
:
A
B
(
a
)
By:
New:[
u
|
v
] Analyze-1
Generated subgoal:
1
3.
u
:
A
4.
v
:
B
(
u
)
<
u
,
v
> = <<
u
,
v
>.1,<
u
,
v
>.2>
a
:
A
B
(
a
)
2
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(4steps total)
PrintForm
NuprlPrimitives
Sections
NuprlLIB
Doc
Type
B(u)
p = <p.1,p.2> 
a:A
