(5steps total)
PrintForm
Definitions
NuprlPrimitives
Sections
NuprlLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
sfa
doc
sexpr
fp
1
1.
A
: Type
2.
X
: Sexpr(
A
)
X
(Sexpr(
A
)
Sexpr(
A
))+
A
By:
AbRecTypeInd Hyp:-1
Generated subgoal:
1
2.
Q
: Sexpr(
A
)
Prop
3.
X
:{
X
:Sexpr(
A
)|
Q
(
X
) }.
X
(Sexpr(
A
)
Sexpr(
A
))+
A
4.
X
: ({
X
:Sexpr(
A
)|
Q
(
X
) }
{
X
:Sexpr(
A
)|
Q
(
X
) })+
A
X
(Sexpr(
A
)
Sexpr(
A
))+
A
Auto
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(5steps total)
PrintForm
Definitions
NuprlPrimitives
Sections
NuprlLIB
Doc
X 
(Sexpr(A)
Sexpr(A))+A X (Sexpr(A)Sexpr(A))+A
Prop
X:{X:Sexpr(A)| Q(X) }. X (Sexpr(A)Sexpr(A))+A
{X:Sexpr(A)| Q(X) })+A
X (Sexpr(A)Sexpr(A))+A
