(7steps total)
PrintForm
NuprlPrimitives
Sections
NuprlLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
sfa
doc
some
via
so
1
2
1.
A
: Type
2.
B
:
A
Prop
3.
C
:Prop. (
x
:
A
.
B
(
x
)
C
)
C
x
:
A
.
B
(
x
)
By:
BackThru: Hyp:-1
Generated subgoal:
1
4.
x
:
A
5.
B
(
x
)
x
:
A
.
B
(
x
)
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(7steps total)
PrintForm
NuprlPrimitives
Sections
NuprlLIB
Doc
Prop
C:Prop. (
C) 
x:A. B(x)
