(3steps total)
PrintForm
Definitions
core
StandardLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
pi2
wf
1
1.
A
: Type
2.
B
:
A
Type
3.
p
:
a
:
A
B
(
a
)
2of(
p
)
B
(1of(
p
))
By:
Analyze 3 THEN RWH pi1_evalC 0
Generated subgoal:
1
3.
a
:
A
4.
p1
:
B
(
a
)
2of(<
a
,
p1
>)
B
(
a
)
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(3steps total)
PrintForm
Definitions
core
StandardLIB
Doc
Type
B(a)
2of(p) 
B(1of(p))Type
B(a)
2of(p) B(1of(p)) 2of(<a,p1>) B(a)
