(12steps total)
PrintForm
Definitions
Lemmas
NuprlPrimitives
Sections
NuprlLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
sfa
doc
ntuple
contains
wf
1
1
1
1.
A
: Type
2.
P
:
A
Prop
3.
n
:
4.
n1
:
.
n1
<
n
(
X
:(
A
^
n1
). (
u
in
X
:
A
^
n1
.
P
(
u
))
Prop)
5.
X
:
A
^
n
6.
n
= 1
X
A
By:
ChangeToEqType:
A
^
n
Generated subgoal:
1
A
= (
A
^
n
)
2
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(12steps total)
PrintForm
Definitions
Lemmas
NuprlPrimitives
Sections
NuprlLIB
Doc
Prop
n1:
(
u in X: A^n1. P(u)) 
Prop)
X 
